1  /-
  2  Copyright (c) 2019 Abhimanyu Pallavi Sudhir. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Abhimanyu Pallavi Sudhir
  5  Construction of the hyperreal numbers as an ultraproduct of real sequences.
  6  -/
  7  
  8  import data.real.basic algebra.field order.filter.filter_product analysis.specific_limits
src         └─────────────┘ └───────────┘ └─────────────────────────┘ └──────────────────────┘
  9  
 10  open filter filter.filter_product
 11  open_locale topological_space classical
 12  
 13  /-- Hyperreal numbers on the ultrafilter extending the cofinite filter -/
 14  @[reducible] def hyperreal := filter.filterprod ℝ (@hyperfilter ℕ)
doc    └───────┘
 15  
 16  namespace hyperreal
 17  
 18  notation `ℝ*` := hyperreal
 19  
 20  private def U : is_ultrafilter (@hyperfilter ℕ) := is_ultrafilter_hyperfilter
 21  noncomputable instance : discrete_linear_ordered_field ℝ* :=
id                            └───────────────────────────┘ └┘
src                           └───────────────────────────┘ └┘
typ                           └───────────────────────────┘ └┘
doc                                                         └┘
 22  filter_product.discrete_linear_ordered_field U
id   └──────────────────────────────────────────┘ 
src  └──────────────────────────────────────────┘ 
typ  └──────────────────────────────────────────┘ 
doc  └──────────────────────────────────────────┘
 23  
 24  /-- A sample infinitesimal hyperreal-/
 25  noncomputable def epsilon : ℝ* := of_seq (λ n, n⁻¹)
id                               └┘    └────┘      └┘
src                              └┘    └────┘        └┘
typ                              └┘    └────┘      └┘
doc                              └┘
 26  
 27  /-- A sample infinite hyperreal-/
 28  noncomputable def omega : ℝ* := of_seq (λ n, n)
id                             └┘    └────┘      
src                            └┘    └────┘
typ                            └┘    └────┘      
doc                            └┘
 29  
 30  localized "notation `ε` := hyperreal.epsilon" in hyperreal
 31  localized "notation `ω` := hyperreal.omega" in hyperreal
 32  
 33  lemma epsilon_eq_inv_omega : ε = ω⁻¹ := rfl
id                                  └┘    └─┘
src                                 └┘    └─┘
typ                                 └┘    └─┘
doc                                  
 34  
 35  lemma inv_epsilon_eq_omega : ε⁻¹ = ω := inv_inv' ω
id                                └┘      └──────┘ 
src                               └┘      └──────┘ 
typ                               └┘      └──────┘ 
doc                                                 
 36  
 37  lemma epsilon_pos : 0 < ε :=
id                          
src                         
typ                         
doc                          
 38  suffices ∀ᶠ i in hyperfilter, (0 : ℝ) < (i : ℕ)⁻¹, by rwa lt_def U,
id            └┘  └┘ └─────────┘              └┘         └────┘ 
src           └┘   └┘ └─────────┘               └┘     └──┘└────┘
typ           └┘  └┘ └─────────┘              └┘     └──┘└────┘
doc           └┘   └┘                                     └──┘      
txt                                                        └──┘      
par                                                        └──┘      
pid                                                                 
st                                                        └───────────┘
 39  have h0' : {n : ℕ | ¬ n > 0} = {0} :=
id                            
src                            
typ                           
 40  by simp only [not_lt, (set.set_of_eq_eq_singleton).symm]; ext; exact nat.le_zero_iff,
id                 └────┘   └────────────────────────┘                    └─────────────┘
src     └─────────┘└────┘└┘ └────────────────────────┘└─────┘  └─┘  └────┘└─────────────┘
typ     └─────────┘└────┘└┘ └────────────────────────┘└─────┘  └─┘  └────┘└─────────────┘
doc     └─────────┘      └┘                           └─────┘  └─┘  └────┘
txt     └─────────┘      └┘                           └─────┘  └─┘  └────┘
par     └─────────┘      └┘                           └─────┘  └─┘  └────┘
pid         └──┘└┘      └┘                           └─────┘            
st     └────────────────────────────────────────────────────────────────────────────────┘
 41  begin
st   └─────
 42    simp only [inv_pos', nat.cast_pos],
id                └──────┘  └──────────┘
src    └─────────┘└──────┘└┘└──────────┘
typ    └─────────┘└──────┘└┘└──────────┘
doc    └─────────┘        └┘            
txt    └─────────┘        └┘            
par    └─────────┘        └┘            
pid        └──┘└┘        └┘            
st   ───────────────────────────────────┘└─
 43    exact mem_hyperfilter_of_finite_compl (by convert set.finite_singleton _),
id           └─────────────────────────────┘             └──────────────────┘
src    └────┘└─────────────────────────────┘   └──────┘└──────────────────┘└┘
typ    └────┘└─────────────────────────────┘   └──────┘└──────────────────┘└┘
doc    └────┘                                  └──────┘                    └┘
txt    └────┘                                  └──────┘                    └┘
par    └────┘                                  └──────┘                    └┘
pid                                           └───────┘                    └─┘
st   ──────────────────────────────────────────┘└─────────────────────────────┘└─
 44  end
st   ──┘
 45  
 46  lemma epsilon_ne_zero : ε ≠ 0 := ne_of_gt epsilon_pos
id                                  └──────┘ └─────────┘
src                                 └──────┘ └─────────┘
typ                                 └──────┘ └─────────┘
doc                          
 47  
 48  lemma omega_pos : 0 < ω := by rw ←inv_epsilon_eq_omega; exact inv_pos epsilon_pos
id                                   └──────────────────┘        └─────┘ └─────────┘
src                              └──┘└──────────────────┘  └────┘└─────┘└─────────┘
typ                              └──┘└──────────────────┘  └────┘└─────┘└─────────┘
doc                               └──┘                      └────┘                  
txt                                └──┘                      └────┘                  
par                                └──┘                      └────┘                  
pid                                  └┘                                             
st                                └────────────────────────────────────────────────────
 49  
src  
typ  
doc  
txt  
par  
pid  
st   
 50  lemma omega_ne_zero : ω ≠ 0 := ne_of_gt omega_pos
id                                └──────┘ └───────┘
src                               └──────┘ └───────┘
typ                               └──────┘ └───────┘
doc                        
 51  
 52  theorem epsilon_mul_omega : ε * ω = 1 := @inv_mul_cancel _ _ ω omega_ne_zero
id                                         └────────────┘      └───────────┘
src                                        └────────────┘      └───────────┘
typ                                        └────────────┘      └───────────┘
doc                                                             
 53  
 54  lemma lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
id                                                   └─────┘  └────┘  
src                                                  └─────┘   └────┘  
typ                                                  └─────┘  └────┘  
doc                                                    └─────┘   └────┘  
 55    ∀ {r : ℝ}, r > 0 → of_seq f < (r : ℝ*) :=
id                     └────┘       └┘
src                     └────┘         └┘
typ                    └────┘       └┘
doc                                       └┘
 56  begin
st   └─────
 57    simp only [metric.tendsto_at_top, dist_zero_right, norm, lt_def U] at hf ⊢,
id                └───────────────────┘  └─────────────┘        └────┘ 
src    └─────────┘└───────────────────┘└┘└─────────────┘└┘    └┘└────┘└───────┘
typ    └─────────┘└───────────────────┘└┘└─────────────┘└┘    └┘└────┘└───────┘
doc    └─────────┘                     └┘               └┘    └┘       └───────┘
txt    └─────────┘                     └┘               └┘    └┘       └───────┘
par    └─────────┘                     └┘               └┘    └┘       └───────┘
pid        └──┘└┘                     └┘               └┘    └┘       └─────┘
st   ───────────────────────────────────────────────────────────────────────────┘└─
 58    intros r hr, cases hf r hr with N hf',
id                        └┘  └┘
src    └─────────┘  └────┘     └─────────┘
typ    └─────────┘  └────┘└┘└┘└─────────┘
doc    └─────────┘  └────┘     └─────────┘
txt    └─────────┘  └────┘     └─────────┘
par    └─────────┘  └────┘     └─────────┘
pid          └───┘            └─────────┘
st   ────────────┘└────────────────────────┘└─
 59    have hs : -{i : ℕ | f i < r} ⊆ {i : ℕ | i ≤ N} :=
id                                          
src    └────────┘ └──┘ └─┘   └┘└──┘ └─┘  └────
typ    └────────┘ └──┘ └─┘ └┘└──┘ └─┘ └────
doc    └────────┘  └──┘ └─┘    └┘  └──┘ └─┘   └────
txt    └────────┘  └──┘ └─┘    └┘  └──┘ └─┘   └────
par    └────────┘  └──┘ └─┘    └┘  └──┘ └─┘   └────
pid    └─────┘└─┘  └──┘ └─┘    └┘  └──┘ └─┘   └───
st   ────────────────────────────────────────────────────
 60      λ i hi1, le_of_lt (by simp only [lt_iff_not_ge];
id                └──────┘                └───────────┘
src  ───┘ └──────┘└──────┘   └─────────┘└───────────┘└─
typ  ───┘ └──────┘└──────┘   └─────────┘└───────────┘└─
doc  ───┘ └──────┘           └─────────┘             └─
txt  ───┘ └──────┘           └─────────┘             └─
par  ───┘ └──────┘           └─────────┘             └─
pid  ───┘ └──────┘           └──────────┘             └──
st   ────────────────────────┘└───────────────────────────
 61      exact λ hi2, hi1 (lt_of_le_of_lt (le_abs_self _) (hf' i hi2)) : i < N),
id                    └─┘  └────────────┘  └─────────┘     └─┘              
src  ───┘└────┘ └────┘    └────────────┘ └─────────┘└──┘        └─┘└┘   
typ  ───┘└────┘ └────┘└─┘ └────────────┘ └─────────┘└──┘ └─┘   └─┘└┘  
doc  ───┘└────┘ └────┘                              └──┘        └─┘└┘   
txt  ───┘└────┘ └────┘                              └──┘        └─┘└┘   
par  ───┘└────┘ └────┘                              └──┘        └─┘└┘   
pid  ─────────┘ └────┘                              └──┘        └───┘   
st   ─────────────────────────────────────────────────────────────────┘└──────┘└─
 62    exact mem_hyperfilter_of_finite_compl
id           └─────────────────────────────┘
src    └────┘└─────────────────────────────┘
typ    └────┘└─────────────────────────────┘
doc    └────┘                               
txt    └────┘                               
par    └────┘                               
pid                                        
st   ────────────────────────────────────────
 63      (set.finite_subset (set.finite_le_nat N) hs)
id        └───────────────┘  └───────────────┘   └┘
src  ───┘ └───────────────┘ └───────────────┘ └┘  └┘
typ  ───┘ └───────────────┘ └───────────────┘└┘└┘└┘
doc  ───┘                                     └┘  └┘
txt  ───┘                                     └┘  └┘
par  ───┘                                     └┘  └┘
pid  ───┘                                     └┘  
st   ────────────────────────────────────────────────┘
 64  end
st   └─┘
 65  
 66  lemma neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
id                                                       └─────┘  └────┘  
src                                                      └─────┘   └────┘  
typ                                                      └─────┘  └────┘  
doc                                                        └─────┘   └────┘  
 67    ∀ {r : ℝ}, r > 0 → (-r : ℝ*) < of_seq f :=
id                         └┘   └────┘ 
src                          └┘   └────┘
typ                        └┘   └────┘ 
doc                             └┘
 68  λ r hr, have hg : _ := hf.neg,
id      └┘                 └┘└──┘
src                           └──┘
typ     └┘                 └┘└──┘
 69  neg_lt_of_neg_lt (by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr)
id   └──────────────┘         └──────┘               └───────────────────────┘ └┘ └┘
src  └──────────────┘     └──┘└──────┘└─────┘  └────┘└───────────────────────┘  
typ  └──────────────┘     └──┘└──────┘└─────┘  └────┘└───────────────────────┘└┘└┘
doc                       └──┘        └─────┘  └────┘                           
txt                       └──┘        └─────┘  └────┘                           
par                       └──┘        └─────┘  └────┘                           
pid                         └┘        └────┘                                  
st                       └───────────┘└───────────────────────────────────────────┘
 70  
 71  lemma gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : tendsto f at_top (𝓝 0)) :
id                                                   └─────┘  └────┘  
src                                                  └─────┘   └────┘  
typ                                                  └─────┘  └────┘  
doc                                                    └─────┘   └────┘  
 72    ∀ {r : ℝ}, r < 0 → (r : ℝ*) < of_seq f :=
id                         └┘   └────┘ 
src                          └┘   └────┘
typ                        └┘   └────┘ 
doc                            └┘
 73  λ r hr, by rw [←of_eq_coe, ←neg_neg r, of_neg];
id      └┘          └───────┘   └─────┘   └────┘
src             └───┘└───────┘└─┘└─────┘ └┘└────┘
typ     └┘     └───┘└───────┘└─┘└─────┘└┘└────┘
doc             └───┘         └─┘        └┘      
txt             └───┘         └─┘        └┘      
par             └───┘         └─┘        └┘      
pid               └─┘         └─┘        └┘      
st             └─────────────┘└──────────┘└──────┘└─
 74  exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)
id         └───────────────────────────┘ └┘  └─────────┘ └┘
src  └────┘└───────────────────────────┘   └─────────┘  └─
typ  └────┘└───────────────────────────┘└┘ └─────────┘└┘└─
doc  └────┘                                             └─
txt  └────┘                                             └─
par  └────┘                                             └─
pid                                                    
st   ────────────────────────────────────────────────────────
 75  
src  
typ  
doc  
txt  
par  
pid  
st   
 76  lemma epsilon_lt_pos (x : ℝ) : x > 0 → ε < of x :=
id                                         └┘ 
src                                         └┘
typ                                        └┘ 
doc                                            └┘
 77  lt_of_tendsto_zero_of_pos tendsto_inverse_at_top_nhds_0_nat
id   └───────────────────────┘ └───────────────────────────────┘
src  └───────────────────────┘ └───────────────────────────────┘
typ  └───────────────────────┘ └───────────────────────────────┘
 78  
 79  /-- Standard part predicate -/
 80  def is_st (x : ℝ*) (r : ℝ) := ∀ δ : ℝ, δ > 0 → (r - δ : ℝ*) < x ∧ x < r + δ
id                  └┘                                └┘         
src                 └┘                                   └┘           
typ                 └┘                                └┘         
doc                 └┘                                       └┘
 81  
 82  /-- Standard part function: like a "round" to ℝ instead of ℤ -/
 83  noncomputable def st : ℝ* → ℝ :=
id                          └┘   
src                         └┘   
typ                         └┘   
doc                         └┘
 84  λ x, if h : ∃ r, is_st x r then classical.some h else 0
id       └┘       └───┘        └────────────┘       
src       └┘        └───┘          └────────────┘        
typ      └┘       └───┘        └────────────┘       
doc                   └───┘
 85  
 86  /-- A hyperreal number is infinitesimal if its standard part is 0 -/
 87  def infinitesimal (x : ℝ*) := is_st x 0
id                          └┘     └───┘ 
src                         └┘     └───┘
typ                         └┘     └───┘ 
doc                         └┘     └───┘
 88  
 89  /-- A hyperreal number is positive infinite if it is larger than all real numbers -/
 90  def infinite_pos (x : ℝ*) := ∀ r : ℝ, x > r
id                         └┘               
src                        └┘               
typ                        └┘               
doc                        └┘
 91  
 92  /-- A hyperreal number is negative infinite if it is smaller than all real numbers -/
 93  def infinite_neg (x : ℝ*) := ∀ r : ℝ, x < r
id                         └┘               
src                        └┘               
typ                        └┘               
doc                        └┘
 94  
 95  /-- A hyperreal number is infinite if it is infinite positive or infinite negative -/
 96  def infinite (x : ℝ*) := infinite_pos x ∨ infinite_neg x
id                     └┘     └──────────┘   └──────────┘ 
src                    └┘     └──────────┘    └──────────┘
typ                    └┘     └──────────┘   └──────────┘ 
doc                    └┘     └──────────┘     └──────────┘
 97  
 98  -- SOME FACTS ABOUT ST
 99  
100  private lemma is_st_unique' (x : ℝ*) (r s : ℝ) (hr : is_st x r) (hs : is_st x s) (hrs : r < s) :
id                                    └┘                 └───┘          └───┘             
src                                   └┘                 └───┘            └───┘               
typ                                   └┘                 └───┘          └───┘             
doc                                   └┘                  └───┘            └───┘
101    false :=
id     └───┘
src    └───┘
typ    └───┘
102  have hrs' : _ := half_pos $ sub_pos_of_lt hrs,
id                    └──────┘   └───────────┘ └─┘
src                   └──────┘   └───────────┘
typ                   └──────┘   └───────────┘ └─┘
103  have hr' : _ := (hr _ hrs').2,
id                    └┘   └──┘ 
src                             
typ                   └┘   └──┘ 
104  have hs' : _ := (hs _ hrs').1,
id                    └┘   └──┘ 
src                             
typ                   └┘   └──┘ 
105  have h : s + -((s - r) / 2) = r + (s - r) / 2 := by linarith,
id                                
src                                              └──────┘
typ                                        └──────┘
doc                                                      └──────┘
txt                                                      └──────┘
par                                                      └──────┘
st                                                     └───────┘
106  by simp only [(of_eq_coe _).symm, sub_eq_add_neg (of s),
id                  └───────┘          └────────────┘  └┘ 
src     └─────────┘ └───────┘└────────┘└────────────┘ └┘ └──
typ     └─────────┘ └───────┘└────────┘└────────────┘ └┘└──
doc     └─────────┘          └────────┘               └┘ └──
txt     └─────────┘          └────────┘                  └──
par     └─────────┘          └────────┘                  └──
pid         └──┘└┘          └────────┘                  └──
st     └──────────────────────────────────────────────────────
107      (of_neg _).symm, (of_add _ _).symm, h] at hr' hs';
id        └────┘           └────┘            
src  ───┘ └────┘└────────┘ └────┘└──────────┘ └──────────┘
typ  ───┘ └────┘└────────┘ └────┘└──────────┘└──────────┘
doc  ───┘       └────────┘       └──────────┘ └──────────┘
txt  ───┘       └────────┘       └──────────┘ └──────────┘
par  ───┘       └────────┘       └──────────┘ └──────────┘
pid  ───┘       └────────┘       └──────────┘ └────────┘
st   ───────────────────────────────────────────────────────
108    exact not_lt_of_lt hs' hr'
id           └──────────┘ └─┘ └─┘
src    └────┘└──────────┘      
typ    └────┘└──────────┘└─┘└─┘
doc    └────┘                  
txt    └────┘                  
par    └────┘                  
pid                           
st   ─────────────────────────────
109  
src  
typ  
doc  
txt  
par  
pid  
st   
110  theorem is_st_unique {x : ℝ*} {r s : ℝ} (hr : is_st x r) (hs : is_st x s) : r = s :=
id                             └┘                 └───┘          └───┘        
src                            └┘                 └───┘            └───┘          
typ                            └┘                 └───┘          └───┘        
doc                            └┘                  └───┘            └───┘
111  begin
st   └─────
112    rcases lt_trichotomy r s with h | h | h,
id            └───────────┘  
src    └─────┘└───────────┘  └─────────────┘
typ    └─────┘└───────────┘└─────────────┘
doc    └─────┘               └─────────────┘
txt    └─────┘               └─────────────┘
par    └─────┘               └─────────────┘
pid                         └─────────────┘
st   ────────────────────────────────────────┘└─
113    { exact false.elim (is_st_unique' x r s hr hs h) },
id             └────────┘  └───────────┘    └┘ └┘ 
src      └────┘└────────┘ └───────────┘        └┘
typ      └────┘└────────┘ └───────────┘└┘└┘└┘
doc      └────┘                                └┘
txt      └────┘                                └┘
par      └────┘                                └┘
pid                                           
st   ───┘└─────────────────────────────────────────────┘└┘
114    { exact h },
id             
src      └────┘ 
typ      └────┘
doc      └────┘ 
txt      └────┘ 
par      └────┘ 
pid            
st   ───┘└──────┘└┘
115    { exact false.elim (is_st_unique' x s r hs hr h) }
id             └────────┘  └───────────┘    └┘ └┘ 
src      └────┘└────────┘ └───────────┘        └┘
typ      └────┘└────────┘ └───────────┘└┘└┘└┘
doc      └────┘                                └┘
txt      └────┘                                └┘
par      └────┘                                └┘
pid                                           
st   ──────────────────────────────────────────────────┘└─
116  end
st   ──┘
117  
118  theorem not_infinite_of_exists_st {x : ℝ*} : (∃ r : ℝ, is_st x r) → ¬ infinite x :=
id                                          └┘           └───┘       └──────┘ 
src                                         └┘           └───┘         └──────┘
typ                                         └┘           └───┘       └──────┘ 
doc                                         └┘              └───┘          └──────┘
119  λ he hi, Exists.dcases_on he $ λ r hr, hi.elim
id     └┘ └┘  └──────────────┘ └┘      └┘  └┘└───┘
src           └──────────────┘                └───┘
typ    └┘ └┘  └──────────────┘ └┘      └┘  └┘└───┘
120     (λ hip, not_lt_of_lt (hr 2 two_pos).2 (hip $ r + 2))
id         └─┘  └──────────┘  └┘   └─────┘    └─┘    
src             └──────────┘       └─────┘            
typ        └─┘  └──────────┘  └┘   └─────┘    └─┘    
121     (λ hin, not_lt_of_lt (hr 2 two_pos).1 (hin $ r - 2))
id         └─┘  └──────────┘  └┘   └─────┘    └─┘    
src             └──────────┘       └─────┘            
typ        └─┘  └──────────┘  └┘   └─────┘    └─┘    
122  
123  theorem is_st_Sup {x : ℝ*} (hni : ¬ infinite x) : is_st x (real.Sup {y : ℝ | of y < x}) :=
id                          └┘          └──────┘     └───┘   └──────┘        └┘   
src                         └┘          └──────┘      └───┘    └──────┘        └┘   
typ                         └┘          └──────┘     └───┘   └──────┘        └┘   
doc                         └┘           └──────┘      └───┘                      └┘
124  let S : set ℝ := {y : ℝ | of y < x} in
id           └─┘            └┘   
src          └─┘            └┘   
typ          └─┘            └┘   
doc                            └┘
125  let R : _ := real.Sup S in
id               └──────┘ 
src               └──────┘
typ              └──────┘ 
126  have hnile : _ := not_forall.mp (not_or_distrib.mp hni).1,
id                     └────────┘└─┘  └────────────┘└─┘ └─┘ 
src                    └────────┘└─┘  └────────────┘└─┘     
typ                    └────────┘└─┘  └────────────┘└─┘ └─┘ 
127  have hnige : _ := not_forall.mp (not_or_distrib.mp hni).2,
id                     └────────┘└─┘  └────────────┘└─┘ └─┘ 
src                    └────────┘└─┘  └────────────┘└─┘     
typ                    └────────┘└─┘  └────────────┘└─┘ └─┘ 
128  Exists.dcases_on hnile $ Exists.dcases_on hnige $ λ r₁ hr₁ r₂ hr₂,
id   └──────────────┘ └───┘   └──────────────┘ └───┘     └┘ └─┘ └┘ └─┘
src  └──────────────┘         └──────────────┘
typ  └──────────────┘ └───┘   └──────────────┘ └───┘     └┘ └─┘ └┘ └─┘
129  have HR₁ : ∃ y : ℝ, y ∈ S :=
id                      
src                     
typ                     
130    ⟨ r₁ - 1, lt_of_lt_of_le (of_lt_of_lt U (sub_one_lt _)) (not_lt.mp hr₁) ⟩,
id       └┘     └────────────┘  └─────────┘   └────────┘      └────┘└─┘ └─┘
src             └────────────┘  └─────────┘   └────────┘      └────┘└─┘
typ      └┘     └────────────┘  └─────────┘   └────────┘      └────┘└─┘ └─┘
131  have HR₂ : ∃ z : ℝ, ∀ y ∈ S, y ≤ z :=
id                             
src                             
typ                            
132    ⟨ r₂, λ y hy, le_of_lt ((of_lt U).mpr (lt_of_lt_of_le hy (not_lt.mp hr₂))) ⟩,
id       └┘     └┘  └──────┘   └───┘  └─┘   └────────────┘ └┘  └────┘└─┘ └─┘
src                  └──────┘   └───┘  └─┘   └────────────┘     └────┘└─┘
typ      └┘     └┘  └──────┘   └───┘  └─┘   └────────────┘ └┘  └────┘└─┘ └─┘
133  λ δ hδ,
id      └┘
typ     └┘
134    ⟨ lt_of_not_ge' $ λ c,
id       └───────────┘     
src      └───────────┘
typ      └───────────┘     
135        have hc : ∀ y ∈ S, y ≤ R - δ := λ y hy, (of_le U.1).mpr $ le_of_lt $ lt_of_lt_of_le hy c,
id                                     └┘   └───┘   └─┘    └──────┘   └────────────┘ └┘ 
src                                               └───┘   └─┘    └──────┘   └────────────┘
typ                                    └┘   └───┘   └─┘    └──────┘   └────────────┘ └┘ 
136        not_lt_of_le ((real.Sup_le _ HR₁ HR₂).mpr hc) $ sub_lt_self R hδ,
id         └──────────┘   └─────────┘   └─┘ └─┘ └─┘  └┘    └─────────┘  └┘
src        └──────────┘   └─────────┘           └─┘        └─────────┘
typ        └──────────┘   └─────────┘   └─┘ └─┘ └─┘  └┘    └─────────┘  └┘
137      lt_of_not_ge' $ λ c,
id       └───────────┘     
src      └───────────┘
typ      └───────────┘     
138        have hc : of (R + δ / 2) < x :=
id                   └┘          
src                  └┘           
typ                  └┘          
doc                  └┘
139          lt_of_lt_of_le (add_lt_add_left (of_lt_of_lt U (half_lt_self hδ)) (of R)) c,
id           └────────────┘  └─────────────┘  └─────────┘   └──────────┘ └┘    └┘    
src          └────────────┘  └─────────────┘  └─────────┘   └──────────┘       └┘
typ          └────────────┘  └─────────────┘  └─────────┘   └──────────┘ └┘    └┘    
doc                                                                             └┘
140        not_lt_of_le (real.le_Sup _ HR₂ hc) $ (lt_add_iff_pos_right _).mpr $ half_pos hδ⟩
id         └──────────┘  └─────────┘   └─┘ └┘     └──────────────────┘   └─┘    └──────┘ └┘
src        └──────────┘  └─────────┘              └──────────────────┘   └─┘    └──────┘
typ        └──────────┘  └─────────┘   └─┘ └┘     └──────────────────┘   └─┘    └──────┘ └┘
141  
142  theorem exists_st_of_not_infinite {x : ℝ*} (hni : ¬ infinite x) : ∃ r : ℝ, is_st x r :=
id                                          └┘          └──────┘           └───┘  
src                                         └┘          └──────┘            └───┘
typ                                         └┘          └──────┘           └───┘  
doc                                         └┘           └──────┘               └───┘
143  ⟨ real.Sup {y : ℝ | of y < x}, is_st_Sup hni ⟩
id     └──────┘        └┘      └───────┘ └─┘
src    └──────┘        └┘        └───────┘
typ    └──────┘        └┘      └───────┘ └─┘
doc                      └┘
144  
145  theorem st_eq_Sup {x : ℝ*} : st x = real.Sup {y : ℝ | of y < x} :=
id                          └┘    └┘   └──────┘        └┘   
src                         └┘    └┘    └──────┘        └┘   
typ                         └┘    └┘   └──────┘        └┘   
doc                         └┘    └┘                       └┘
146  begin
st   └─────
147  unfold st, split_ifs,
src  └───────┘  └───────┘
typ  └───────┘  └───────┘
doc  └───────┘  └───────┘
txt  └───────┘  └───────┘
par  └───────┘  └───────┘
pid        └─┘
st   ────────┘└─────────┘└─
148  { exact is_st_unique (classical.some_spec h) (is_st_Sup (not_infinite_of_exists_st h)) },
id           └──────────┘  └─────────────────┘     └───────┘  └───────────────────────┘ 
src    └────┘└──────────┘ └─────────────────┘ └┘ └───────┘ └───────────────────────┘ └─┘
typ    └────┘└──────────┘ └─────────────────┘ └┘ └───────┘ └───────────────────────┘└─┘
doc    └────┘                                 └┘                                     └─┘
txt    └────┘                                 └┘                                     └─┘
par    └────┘                                 └┘                                     └─┘
pid                                          └┘                                     └┘
st   ─┘└───────────────────────────────────────────────────────────────────────────────────┘└┘
149  { cases not_imp_comm.mp exists_st_of_not_infinite h with H H,
id           └─────────────┘ └───────────────────────┘ 
src    └────┘└─────────────┘└───────────────────────┘ └───────┘
typ    └────┘└─────────────┘└───────────────────────┘└───────┘
doc    └────┘                                         └───────┘
txt    └────┘                                         └───────┘
par    └────┘                                         └───────┘
pid                                                  └───────┘
st   ───────────────────────────────────────────────────────────┘└─
150    { rw (set.ext (λ i, ⟨λ hi, set.mem_univ i, λ hi, H i⟩) : {y : ℝ | of y < x} = set.univ),
id           └─────┘              └──────────┘                         └┘       └──────┘
src      └─┘ └─────┘  └──┘  └───┘└──────────┘ └┘ └───┘  └───┘└──┘ └─┘└┘  └┘└──────┘
typ      └─┘ └─────┘  └──┘  └───┘└──────────┘ └┘ └───┘ └───┘└──┘ └─┘└┘ └┘└──────┘
doc      └─┘          └──┘  └───┘             └┘ └───┘  └───┘ └──┘ └─┘└┘   └┘         
txt      └─┘          └──┘  └───┘             └┘ └───┘  └───┘ └──┘ └─┘     └┘         
par      └─┘          └──┘  └───┘             └┘ └───┘  └───┘ └──┘ └─┘     └┘         
pid                  └──┘  └───┘             └┘ └───┘  └───┘ └──┘ └─┘     └┘         
st   ───┘└───────────────────────────────────────────────────────────────────────────────────┘└─
151      exact (real.Sup_univ).symm },
id              └───────────┘
src      └────┘ └───────────┘└─────┘
typ      └────┘ └───────────┘└─────┘
doc      └────┘              └─────┘
txt      └────┘              └─────┘
par      └────┘              └─────┘
pid                         └───┘└┘
st   ──────────────────────────────┘└┘
152    { rw (set.ext (λ i, ⟨λ hi, false.elim (not_lt_of_lt (H i) hi),
id           └─────┘                          └──────────┘  
src      └─┘ └─────┘  └──┘  └───┘           └──────────┘   └┘  └──
typ      └─┘ └─────┘  └──┘  └───┘           └──────────┘  └┘  └──
doc      └─┘          └──┘  └───┘                          └┘  └──
txt      └─┘          └──┘  └───┘                          └┘  └──
par      └─┘          └──┘  └───┘                          └┘  └──
pid                  └──┘  └───┘                          └┘  └──
st   ─────────────────────────────────────────────────────────────────
153      λ hi, false.elim (set.not_mem_empty i hi)⟩) : {y : ℝ | of y < x} = ∅),
id             └────────┘  └───────────────┘                   └┘         
src  ───┘ └───┘└────────┘ └───────────────┘   └────┘└──┘ └─┘└┘   └┘ 
typ  ───┘ └───┘└────────┘ └───────────────┘   └────┘└──┘ └─┘└┘  └┘ 
doc  ───┘ └───┘                               └────┘ └──┘ └─┘└┘   └┘  
txt  ───┘ └───┘                               └────┘ └──┘ └─┘     └┘  
par  ───┘ └───┘                               └────┘ └──┘ └─┘     └┘  
pid  ───┘ └───┘                               └────┘ └──┘ └─┘     └┘  
st   ────────────────────────────────────────────────────────────────────────┘└─
154      exact (real.Sup_empty).symm } }
id              └────────────┘
src      └────┘ └────────────┘└─────┘
typ      └────┘ └────────────┘└─────┘
doc      └────┘               └─────┘
txt      └────┘               └─────┘
par      └────┘               └─────┘
pid                          └───┘└┘
st   ───────────────────────────────┘└───
155  end
st   ──┘
156  
157  theorem exists_st_iff_not_infinite {x : ℝ*} : (∃ r : ℝ, is_st x r) ↔ ¬ infinite x :=
id                                           └┘           └───┘      └──────┘ 
src                                          └┘           └───┘        └──────┘
typ                                          └┘           └───┘      └──────┘ 
doc                                          └┘              └───┘          └──────┘
158  ⟨ not_infinite_of_exists_st, exists_st_of_not_infinite ⟩
id     └───────────────────────┘  └───────────────────────┘
src    └───────────────────────┘  └───────────────────────┘
typ    └───────────────────────┘  └───────────────────────┘
159  
160  theorem infinite_iff_not_exists_st {x : ℝ*} : infinite x ↔ ¬ ∃ r : ℝ, is_st x r :=
id                                           └┘    └──────┘          └───┘  
src                                          └┘    └──────┘           └───┘
typ                                          └┘    └──────┘          └───┘  
doc                                          └┘    └──────┘                └───┘
161  iff_not_comm.mp exists_st_iff_not_infinite
id   └──────────┘└─┘ └────────────────────────┘
src  └──────────┘└─┘ └────────────────────────┘
typ  └──────────┘└─┘ └────────────────────────┘
162  
163  theorem st_infinite {x : ℝ*} (hi : infinite x) : st x = 0 :=
id                            └┘        └──────┘     └┘  
src                           └┘        └──────┘      └┘   
typ                           └┘        └──────┘     └┘  
doc                           └┘        └──────┘      └┘
164  begin
st   └─────
165    unfold st, split_ifs,
src    └───────┘  └───────┘
typ    └───────┘  └───────┘
doc    └───────┘  └───────┘
txt    └───────┘  └───────┘
par    └───────┘  └───────┘
pid          └─┘
st   ──────────┘└─────────┘└─
166    { exact false.elim ((infinite_iff_not_exists_st.mp hi) h) },
id             └────────┘   └───────────────────────────┘ └┘  
src      └────┘└────────┘  └───────────────────────────┘  └┘ └┘
typ      └────┘└────────┘  └───────────────────────────┘└┘└┘└┘
doc      └────┘                                           └┘ └┘
txt      └────┘                                           └┘ └┘
par      └────┘                                           └┘ └┘
pid                                                      └┘ 
st   ───┘└──────────────────────────────────────────────────────┘└┘
167    { refl }
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
pid          
st   ────────┘└─
168  end
st   ──┘
169  
170  lemma st_of_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : st x = r :=
id                          └┘                └───┘      └┘   
src                         └┘                └───┘        └┘   
typ                         └┘                └───┘      └┘   
doc                         └┘                 └───┘        └┘
171  begin
st   └─────
172    unfold st, split_ifs,
src    └───────┘  └───────┘
typ    └───────┘  └───────┘
doc    └───────┘  └───────┘
txt    └───────┘  └───────┘
par    └───────┘  └───────┘
pid          └─┘
st   ──────────┘└─────────┘└─
173    { exact is_st_unique (classical.some_spec h) hxr },
id             └──────────┘  └─────────────────┘   └─┘
src      └────┘└──────────┘ └─────────────────┘ └┘   
typ      └────┘└──────────┘ └─────────────────┘└┘└─┘
doc      └────┘                                 └┘   
txt      └────┘                                 └┘   
par      └────┘                                 └┘   
pid                                            └┘   
st   ───┘└─────────────────────────────────────────────┘└┘
174    { exact false.elim (h ⟨r, hxr⟩) }
id             └────────┘      └─┘
src      └────┘└────────┘    └┘   └─┘
typ      └────┘└────────┘  └┘└─┘└─┘
doc      └────┘              └┘   └─┘
txt      └────┘              └┘   └─┘
par      └────┘              └┘   └─┘
pid                         └┘   └┘
st   ─────────────────────────────────┘└─
175  end
st   ──┘
176  
177  lemma is_st_st_of_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : is_st x (st x) :=
id                                └┘                └───┘      └───┘   └┘ 
src                               └┘                └───┘        └───┘    └┘
typ                               └┘                └───┘      └───┘   └┘ 
doc                               └┘                 └───┘        └───┘    └┘
178  by rwa [st_of_is_st hxr]
id           └─────────┘ └─┘
src     └───┘└─────────┘   └─
typ     └───┘└─────────┘└─┘└─
doc     └───┘              └─
txt     └───┘              └─
par     └───┘              └─
pid        └┘              
st     └───────────────────┘
179  
src  
typ  
doc  
txt  
par  
pid  
st   
180  lemma is_st_st_of_exists_st {x : ℝ*} (hx : ∃ r : ℝ, is_st x r) : is_st x (st x) :=
id                                    └┘              └───┘      └───┘   └┘ 
src                                   └┘              └───┘        └───┘    └┘
typ                                   └┘              └───┘      └───┘   └┘ 
doc                                   └┘                 └───┘        └───┘    └┘
181  Exists.dcases_on hx (λ r, is_st_st_of_is_st)
id   └──────────────┘ └┘      └───────────────┘
src  └──────────────┘          └───────────────┘
typ  └──────────────┘ └┘      └───────────────┘
182  
183  lemma is_st_st {x : ℝ*} (hx : st x ≠ 0) : is_st x (st x) :=
id                       └┘        └┘        └───┘   └┘ 
src                      └┘        └┘         └───┘    └┘
typ                      └┘        └┘        └───┘   └┘ 
doc                      └┘        └┘          └───┘    └┘
184  begin
st   └─────
185    unfold st, split_ifs,
src    └───────┘  └───────┘
typ    └───────┘  └───────┘
doc    └───────┘  └───────┘
txt    └───────┘  └───────┘
par    └───────┘  └───────┘
pid          └─┘
st   ──────────┘└─────────┘└─
186    { exact classical.some_spec h },
id             └─────────────────┘ 
src      └────┘└─────────────────┘ 
typ      └────┘└─────────────────┘
doc      └────┘                    
txt      └────┘                    
par      └────┘                    
pid                               
st   ───┘└──────────────────────────┘└┘
187    { exact false.elim (hx (by unfold st; split_ifs; refl)) }
id             └────────┘  └┘
src      └────┘└────────┘      └───────┘└┘└───────┘└┘└──┘└─┘
typ      └────┘└────────┘ └┘   └───────┘└┘└───────┘└┘└──┘└─┘
doc      └────┘                └───────┘└┘└───────┘└┘└──┘└─┘
txt      └────┘                └───────┘└┘└───────┘└┘└──┘└─┘
par      └────┘                └───────┘└┘└───────┘└┘└──┘└─┘
pid                           └───────────────────────────┘
st   ───────────────────────────┘└─────────────────────────┘└─┘└─
188  end
st   ──┘
189  
190  lemma is_st_st' {x : ℝ*} (hx : ¬ infinite x) : is_st x (st x) :=
id                        └┘         └──────┘     └───┘   └┘ 
src                       └┘         └──────┘      └───┘    └┘
typ                       └┘         └──────┘     └───┘   └┘ 
doc                       └┘          └──────┘      └───┘    └┘
191  is_st_st_of_exists_st $ exists_st_of_not_infinite hx
id   └───────────────────┘   └───────────────────────┘ └┘
src  └───────────────────┘   └───────────────────────┘
typ  └───────────────────┘   └───────────────────────┘ └┘
192  
193  lemma is_st_refl_real (r : ℝ) : is_st r r :=
id                                  └───┘  
src                                 └───┘
typ                                 └───┘  
doc                                  └───┘
194  λ δ hδ, ⟨ sub_lt_self _ (of_lt_of_lt U hδ), (lt_add_of_pos_right _ (of_lt_of_lt U hδ)) ⟩
id      └┘    └─────────┘    └─────────┘  └┘    └─────────────────┘    └─────────┘  └┘
src            └─────────┘    └─────────┘        └─────────────────┘    └─────────┘ 
typ     └┘    └─────────┘    └─────────┘  └┘    └─────────────────┘    └─────────┘  └┘
195  
196  lemma st_id_real (r : ℝ) : st r = r := st_of_is_st (is_st_refl_real r)
id                             └┘       └─────────┘  └─────────────┘ 
src                            └┘         └─────────┘  └─────────────┘
typ                            └┘       └─────────┘  └─────────────┘ 
doc                             └┘
197  
198  lemma eq_of_is_st_real {r s : ℝ} : is_st r s → r = s := is_st_unique (is_st_refl_real r)
id                                     └───┘           └──────────┘  └─────────────┘ 
src                                    └───┘               └──────────┘  └─────────────┘
typ                                    └───┘           └──────────┘  └─────────────┘ 
doc                                     └───┘
199  
200  lemma is_st_real_iff_eq {r s : ℝ} : is_st r s ↔ r = s :=
id                                      └───┘      
src                                     └───┘        
typ                                     └───┘      
doc                                      └───┘
201  ⟨eq_of_is_st_real, λ hrs, by rw [hrs]; exact is_st_refl_real s⟩
id    └──────────────┘    └─┘         └─┘         └─────────────┘ 
src   └──────────────┘            └──┘     └────┘└─────────────┘
typ   └──────────────┘    └─┘     └──┘└─┘  └────┘└─────────────┘
doc                               └──┘     └────┘               
txt                               └──┘     └────┘               
par                               └──┘     └────┘               
pid                                 └┘                         
st                               └──────┘└───────────────────────┘
202  
203  lemma is_st_symm_real {r s : ℝ} : is_st r s ↔ is_st s r :=
id                                    └───┘    └───┘  
src                                   └───┘      └───┘
typ                                   └───┘    └───┘  
doc                                    └───┘       └───┘
204  by rw [is_st_real_iff_eq, is_st_real_iff_eq, eq_comm]
id          └───────────────┘  └───────────────┘  └─────┘
src     └──┘└───────────────┘└┘└───────────────┘└┘└─────┘└─
typ     └──┘└───────────────┘└┘└───────────────┘└┘└─────┘└─
doc     └──┘                 └┘                 └┘       └─
txt     └──┘                 └┘                 └┘       └─
par     └──┘                 └┘                 └┘       └─
pid       └┘                 └┘                 └┘       
st     └────────────────────┘└─────────────────┘└───────┘
205  
src  
typ  
doc  
txt  
par  
pid  
st   
206  lemma is_st_trans_real {r s t : ℝ} : is_st r s → is_st s t → is_st r t :=
id                                       └───┘     └───┘     └───┘  
src                                      └───┘       └───┘       └───┘
typ                                      └───┘     └───┘     └───┘  
doc                                       └───┘       └───┘       └───┘
207  by rw [is_st_real_iff_eq, is_st_real_iff_eq, is_st_real_iff_eq]; exact eq.trans
id          └───────────────┘  └───────────────┘  └───────────────┘         └──────┘
src     └──┘└───────────────┘└┘└───────────────┘└┘└───────────────┘  └────┘└──────┘
typ     └──┘└───────────────┘└┘└───────────────┘└┘└───────────────┘  └────┘└──────┘
doc     └──┘                 └┘                 └┘                   └────┘        
txt     └──┘                 └┘                 └┘                   └────┘        
par     └──┘                 └┘                 └┘                   └────┘        
pid       └┘                 └┘                 └┘                                
st     └────────────────────┘└─────────────────┘└─────────────────┘└────────────────
208  
src  
typ  
doc  
txt  
par  
pid  
st   
209  lemma is_st_inj_real {r₁ r₂ s : ℝ} (h1 : is_st r₁ s) (h2 : is_st r₂ s) : r₁ = r₂ :=
id                                           └───┘ └┘         └───┘ └┘     └┘  └┘
src                                          └───┘             └───┘            
typ                                          └───┘ └┘         └───┘ └┘     └┘  └┘
doc                                           └───┘             └───┘
210  eq.trans (eq_of_is_st_real h1) (eq_of_is_st_real h2).symm
id   └──────┘  └──────────────┘ └┘   └──────────────┘ └┘ └──┘
src  └──────┘  └──────────────┘      └──────────────┘    └──┘
typ  └──────┘  └──────────────┘ └┘   └──────────────┘ └┘ └──┘
211  
212  lemma is_st_iff_abs_sub_lt_delta {x : ℝ*} {r : ℝ} :
id                                         └┘       
src                                        └┘       
typ                                        └┘       
doc                                        └┘
213    is_st x r ↔ ∀ (δ : ℝ), δ > 0 → abs (x - r) < δ :=
id     └───┘                    └─┘       
src    └───┘                       └─┘        
typ    └───┘                    └─┘       
doc    └───┘
214  by simp only [abs_sub_lt_iff, @sub_lt _ _ (r : ℝ*) x _,
id                 └────────────┘   └────┘             
src     └─────────┘└────────────┘└┘ └────┘└───┘  └─┘  └┘ └───
typ     └─────────┘└────────────┘└┘ └────┘└───┘ └─┘  └┘└───
doc     └─────────┘              └┘       └───┘  └─┘  └┘ └───
txt     └─────────┘              └┘       └───┘  └─┘  └┘ └───
par     └─────────┘              └┘       └───┘  └─┘  └┘ └───
pid         └──┘└┘              └┘       └───┘  └─┘  └┘ └───
st     └─────────────────────────────────────────────────────
215      @sub_lt_iff_lt_add' _ _ x (r : ℝ*) _, and_comm]; refl
id        └────────────────┘                 └──────┘
src  ───┘ └────────────────┘└───┘   └─┘  └───┘└──────┘  └────
typ  ───┘ └────────────────┘└───┘ └─┘  └───┘└──────┘  └────
doc  ───┘                   └───┘   └─┘  └───┘          └────
txt  ───┘                   └───┘   └─┘  └───┘          └────
par  ───┘                   └───┘   └─┘  └───┘          └────
pid  ───┘                   └───┘   └─┘  └───┘              
st   ──────────────────────────────────────────────────────────
216  
src  
typ  
doc  
txt  
par  
pid  
st   
217  lemma is_st_add {x y : ℝ*} {r s : ℝ} : is_st x r → is_st y s → is_st (x + y) (r + s) :=
id                          └┘             └───┘     └───┘     └───┘         
src                         └┘             └───┘       └───┘       └───┘           
typ                         └┘             └───┘     └───┘     └───┘         
doc                         └┘              └───┘       └───┘       └───┘
218  λ hxr hys d hd,
id     └─┘ └─┘  └┘
typ    └─┘ └─┘  └┘
219  have hxr' : _ := hxr (d / 2) (half_pos hd), have hys' : _ := hys (d / 2) (half_pos hd),
id                    └─┘        └──────┘ └┘                    └─┘        └──────┘ └┘
src                               └──────┘                                   └──────┘
typ                   └─┘        └──────┘ └┘                    └─┘        └──────┘ └┘
220  by rw [←of_eq_coe, ←of_eq_coe, ←add_halves d, of_add, of_add, add_sub_comm,
id           └───────┘   └───────┘   └────────┘   └────┘  └────┘  └──────────┘
src     └───┘└───────┘└─┘└───────┘└─┘└────────┘ └┘└────┘└┘└────┘└┘└──────────┘└─
typ     └───┘└───────┘└─┘└───────┘└─┘└────────┘└┘└────┘└┘└────┘└┘└──────────┘└─
doc     └───┘         └─┘         └─┘           └┘      └┘      └┘            └─
txt     └───┘         └─┘         └─┘           └┘      └┘      └┘            └─
par     └───┘         └─┘         └─┘           └┘      └┘      └┘            └─
pid       └─┘         └─┘         └─┘           └┘      └┘      └┘            └─
st     └─────────────┘└──────────┘└─────────────┘└──────┘└──────┘└────────────┘└─
221         norm_num.add_comm_middle, ←add_assoc, add_assoc _ _ (of s), add_comm _ (of s)];
id          └──────────────────────┘   └───────┘  └───────┘      └┘    └──────┘    └┘ 
src  ──────┘└──────────────────────┘└─┘└───────┘└┘└───────┘└───┘ └┘ └─┘└──────┘└─┘ └┘ └┘
typ  ──────┘└──────────────────────┘└─┘└───────┘└┘└───────┘└───┘ └┘└─┘└──────┘└─┘ └┘└┘
doc  ──────┘                        └─┘         └┘         └───┘ └┘ └─┘        └─┘ └┘ └┘
txt  ──────┘                        └─┘         └┘         └───┘    └─┘        └─┘    └┘
par  ──────┘                        └─┘         └┘         └───┘    └─┘        └─┘    └┘
pid  ──────┘                        └─┘         └┘         └───┘    └─┘        └─┘    └┘
st   ──────────────────────────────┘└──────────┘└────────────────────┘└─────────────────┘└─
222  exact ⟨ add_lt_add hxr'.1 hys'.1, add_lt_add hxr'.2 hys'.2 ⟩
id                                     └────────┘ └──┘   └──┘
src  └────┘               └─┘    └──┘└────────┘    └─┘    └────
typ  └────┘               └─┘    └──┘└────────┘└──┘└─┘└──┘└────
doc  └────┘               └─┘    └──┘              └─┘    └────
txt  └────┘               └─┘    └──┘              └─┘    └────
par  └────┘               └─┘    └──┘              └─┘    └────
pid                      └─┘    └──┘              └─┘    └──┘
st   ─────────────────────────────────────────────────────────────
223  
src  
typ  
doc  
txt  
par  
pid  
st   
224  lemma is_st_neg {x : ℝ*} {r : ℝ} (hxr : is_st x r) : is_st (-x) (-r) :=
id                        └┘                └───┘      └───┘     
src                       └┘                └───┘        └───┘      
typ                       └┘                └───┘      └───┘     
doc                       └┘                 └───┘        └───┘
225  λ d hd, by show -(r : ℝ*) - d < -x ∧ -x < -r + d; cases (hxr d hd); split; linarith
id      └┘                                            └─┘  └┘
src             └───┘  └─┘  └┘            └────┘         └───┘  └────────
typ     └┘     └───┘  └─┘  └┘         └────┘ └─┘└┘  └───┘  └────────
doc             └───┘   └─┘  └┘               └────┘         └───┘  └────────
txt             └───┘   └─┘  └┘               └────┘         └───┘  └────────
par             └───┘   └─┘  └┘               └────┘         └───┘  └────────
pid             └───┘   └─┘  └┘                                            
st             └─────────────────────────────────────────────────────────────────────────
226  
src  
typ  
doc  
txt  
par  
pid  
st   
227  lemma is_st_sub {x y : ℝ*} {r s : ℝ} : is_st x r → is_st y s → is_st (x - y) (r - s) :=
id                          └┘             └───┘     └───┘     └───┘         
src                         └┘             └───┘       └───┘       └───┘           
typ                         └┘             └───┘     └───┘     └───┘         
doc                         └┘              └───┘       └───┘       └───┘
228  λ hxr hys, by rw [sub_eq_add_neg, sub_eq_add_neg]; exact is_st_add hxr (is_st_neg hys)
id     └─┘ └─┘         └────────────┘  └────────────┘         └───────┘ └─┘  └───────┘ └─┘
src                └──┘└────────────┘└┘└────────────┘  └────┘└───────┘    └───────┘   └─
typ    └─┘ └─┘     └──┘└────────────┘└┘└────────────┘  └────┘└───────┘└─┘ └───────┘└─┘└─
doc                └──┘              └┘                └────┘                         └─
txt                └──┘              └┘                └────┘                         └─
par                └──┘              └┘                └────┘                         └─
pid                  └┘              └┘                                              
st                └─────────────────┘└──────────────┘└─────────────────────────────────────
229  
src  
typ  
doc  
txt  
par  
pid  
st   
230  /- (st x < st y) → (x < y) → (x ≤ y) → (st x ≤ st y) -/
src  ────────────────────────────────────────────────────────
typ  ────────────────────────────────────────────────────────
doc  ────────────────────────────────────────────────────────
txt  ────────────────────────────────────────────────────────
par  ────────────────────────────────────────────────────────
pid  ────────────────────────────────────────────────────────
st   ────────────────────────────────────────────────────────
231  
src  
typ  
doc  
txt  
par  
pid  
st   
232  lemma lt_of_is_st_lt {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) :
id                               └┘                  └───┘           └───┘  
src                              └┘                  └───┘             └───┘
typ                              └┘                  └───┘           └───┘  
doc                              └┘                   └───┘             └───┘
233    r < s → x < y :=
id            
src             
typ           
234  λ hrs, have hrs' : 0 < (s - r) / 2 := half_pos (sub_pos.mpr hrs),
id     └─┘                            └──────┘  └─────┘└──┘ └─┘
src                                     └──────┘  └─────┘└──┘
typ    └─┘                            └──────┘  └─────┘└──┘ └─┘
235  have hxr' : _ := (hxr _ hrs').2, have hys' : _ := (hys _ hrs').1,
id                     └─┘   └──┘                      └─┘   └──┘ 
src                                                               
typ                    └─┘   └──┘                      └─┘   └──┘ 
236  have H1 : r + ((s - r) / 2) = (r + s) / 2 := by linarith,
id                               
src                                            └──────┘
typ                                       └──────┘
doc                                                  └──────┘
txt                                                  └──────┘
par                                                  └──────┘
st                                                  └───────┘
237  have H2 : s - ((s - r) / 2) = (r + s) / 2 := by linarith,
id                               
src                                            └──────┘
typ                                       └──────┘
doc                                                  └──────┘
txt                                                  └──────┘
par                                                  └──────┘
st                                                  └───────┘
238  by simp only [(of_eq_coe _).symm, (of_add _ _).symm, (of_sub _ _).symm, H1, H2] at hxr' hys';
id                  └───────┘           └────┘             └────┘            └┘  └┘
src     └─────────┘ └───────┘└────────┘ └────┘└──────────┘ └────┘└──────────┘  └┘  └────────────┘
typ     └─────────┘ └───────┘└────────┘ └────┘└──────────┘ └────┘└──────────┘└┘└┘└┘└────────────┘
doc     └─────────┘          └────────┘       └──────────┘       └──────────┘  └┘  └────────────┘
txt     └─────────┘          └────────┘       └──────────┘       └──────────┘  └┘  └────────────┘
par     └─────────┘          └────────┘       └──────────┘       └──────────┘  └┘  └────────────┘
pid         └──┘└┘          └────────┘       └──────────┘       └──────────┘  └┘  └──────────┘
st     └───────────────────────────────────────────────────────────────────────────────────────────
239  exact lt_trans hxr' hys'
id         └──────┘ └──┘ └──┘
src  └────┘└──────┘        
typ  └────┘└──────┘└──┘└──┘
doc  └────┘                
txt  └────┘                
par  └────┘                
pid                       
st   ─────────────────────────
240  
src  
typ  
doc  
txt  
par  
pid  
st   
241  lemma is_st_le_of_le {x y : ℝ*} {r s : ℝ} (hrx : is_st x r) (hsy : is_st y s) :
id                               └┘                  └───┘           └───┘  
src                              └┘                  └───┘             └───┘
typ                              └┘                  └───┘           └───┘  
doc                              └┘                   └───┘             └───┘
242    x ≤ y → r ≤ s := by rw [←not_lt, ←not_lt, not_imp_not]; exact lt_of_is_st_lt hsy hrx
id                        └────┘   └────┘  └─────────┘         └────────────┘ └─┘ └─┘
src                      └───┘└────┘└─┘└────┘└┘└─────────┘  └────┘└────────────┘      
typ                  └───┘└────┘└─┘└────┘└┘└─────────┘  └────┘└────────────┘└─┘└─┘
doc                        └───┘      └─┘      └┘             └────┘                    
txt                        └───┘      └─┘      └┘             └────┘                    
par                        └───┘      └─┘      └┘             └────┘                    
pid                          └─┘      └─┘      └┘                                      
st                        └──────────┘└───────┘└───────────┘└──────────────────────────────
243  
src  
typ  
doc  
txt  
par  
pid  
st   
244  lemma st_le_of_le {x y : ℝ*} (hix : ¬ infinite x) (hiy : ¬ infinite y) :
id                            └┘          └──────┘           └──────┘ 
src                           └┘          └──────┘            └──────┘
typ                           └┘          └──────┘           └──────┘ 
doc                           └┘           └──────┘             └──────┘
245    x ≤ y → st x ≤ st y :=
id          └┘   └┘ 
src           └┘    └┘
typ         └┘   └┘ 
doc            └┘     └┘
246  have hx' : _ := is_st_st' hix, have hy' : _ := is_st_st' hiy,
id                   └───────┘ └─┘                  └───────┘ └─┘
src                  └───────┘                      └───────┘
typ                  └───────┘ └─┘                  └───────┘ └─┘
247  is_st_le_of_le hx' hy'
id   └────────────┘ └─┘ └─┘
src  └────────────┘
typ  └────────────┘ └─┘ └─┘
248  
249  lemma lt_of_st_lt {x y : ℝ*} (hix : ¬ infinite x) (hiy : ¬ infinite y) :
id                            └┘          └──────┘           └──────┘ 
src                           └┘          └──────┘            └──────┘
typ                           └┘          └──────┘           └──────┘ 
doc                           └┘           └──────┘             └──────┘
250    st x < st y → x < y :=
id     └┘   └┘      
src    └┘    └┘       
typ    └┘   └┘      
doc    └┘     └┘
251  have hx' : _ := is_st_st' hix, have hy' : _ := is_st_st' hiy,
id                   └───────┘ └─┘                  └───────┘ └─┘
src                  └───────┘                      └───────┘
typ                  └───────┘ └─┘                  └───────┘ └─┘
252  lt_of_is_st_lt hx' hy'
id   └────────────┘ └─┘ └─┘
src  └────────────┘
typ  └────────────┘ └─┘ └─┘
253  
254  -- BASIC LEMMAS ABOUT INFINITE
255  
256  lemma infinite_pos_def {x : ℝ*} : infinite_pos x ↔ ∀ r : ℝ, x > r := by rw iff_eq_eq; refl
id                               └┘    └──────────┘                       └───────┘
src                              └┘    └──────────┘                       └─┘└───────┘  └────
typ                              └┘    └──────────┘                    └─┘└───────┘  └────
doc                              └┘    └──────────┘                          └─┘           └────
txt                                                                          └─┘           └────
par                                                                          └─┘           └────
pid                                                                                           
st                                                                          └───────────────────
257  
src  
typ  
doc  
txt  
par  
pid  
st   
258  lemma infinite_neg_def {x : ℝ*} : infinite_neg x ↔ ∀ r : ℝ, x < r := by rw iff_eq_eq; refl
id                               └┘    └──────────┘                       └───────┘
src                              └┘    └──────────┘                       └─┘└───────┘  └────
typ                              └┘    └──────────┘                    └─┘└───────┘  └────
doc                              └┘    └──────────┘                          └─┘           └────
txt                                                                          └─┘           └────
par                                                                          └─┘           └────
pid                                                                                           
st                                                                          └───────────────────
259  
src  
typ  
doc  
txt  
par  
pid  
st   
260  lemma ne_zero_of_infinite {x : ℝ*} : infinite x → x ≠ 0 :=
id                                  └┘    └──────┘     
src                                 └┘    └──────┘       
typ                                 └┘    └──────┘     
doc                                 └┘    └──────┘
261  λ hI h0, or.cases_on hI
id     └┘ └┘  └─────────┘ └┘
src           └─────────┘
typ    └┘ └┘  └─────────┘ └┘
262    (λ hip, lt_irrefl (0 : ℝ*) ((by rwa ←h0 : infinite_pos 0) 0))
id        └─┘  └───────┘      └┘            └┘   └──────────┘
src            └───────┘      └┘       └───┘    └──────────┘
typ       └─┘  └───────┘      └┘       └───┘└┘  └──────────┘
doc                           └┘       └───┘    └──────────┘
txt                                    └───┘  
par                                    └───┘  
pid                                       └┘  
st                                    └───────┘
263    (λ hin, lt_irrefl (0 : ℝ*) ((by rwa ←h0 : infinite_neg 0) 0))
id        └─┘  └───────┘      └┘            └┘   └──────────┘
src            └───────┘      └┘       └───┘    └──────────┘
typ       └─┘  └───────┘      └┘       └───┘└┘  └──────────┘
doc                           └┘       └───┘    └──────────┘
txt                                    └───┘  
par                                    └───┘  
pid                                       └┘  
st                                    └───────┘
264  
265  lemma not_infinite_zero : ¬ infinite 0 := λ hI, ne_zero_of_infinite hI rfl
id                              └──────┘        └┘  └─────────────────┘ └┘ └─┘
src                             └──────┘            └─────────────────┘    └─┘
typ                             └──────┘        └┘  └─────────────────┘ └┘ └─┘
doc                              └──────┘
266  
267  lemma pos_of_infinite_pos {x : ℝ*} : infinite_pos x → x > 0 := λ hip, hip 0
id                                  └┘    └──────────┘             └─┘  └─┘
src                                 └┘    └──────────┘       
typ                                 └┘    └──────────┘             └─┘  └─┘
doc                                 └┘    └──────────┘
268  
269  lemma neg_of_infinite_neg {x : ℝ*} : infinite_neg x → x < 0 := λ hin, hin 0
id                                  └┘    └──────────┘             └─┘  └─┘
src                                 └┘    └──────────┘       
typ                                 └┘    └──────────┘             └─┘  └─┘
doc                                 └┘    └──────────┘
270  
271  lemma not_infinite_pos_of_infinite_neg {x : ℝ*} : infinite_neg x → ¬ infinite_pos x :=
id                                               └┘    └──────────┘     └──────────┘ 
src                                              └┘    └──────────┘      └──────────┘
typ                                              └┘    └──────────┘     └──────────┘ 
doc                                              └┘    └──────────┘       └──────────┘
272  λ hn hp, not_lt_of_lt (hn 1) (hp 1)
id     └┘ └┘  └──────────┘  └┘     └┘
src           └──────────┘
typ    └┘ └┘  └──────────┘  └┘     └┘
273  
274  lemma not_infinite_neg_of_infinite_pos {x : ℝ*} : infinite_pos x → ¬ infinite_neg x :=
id                                               └┘    └──────────┘     └──────────┘ 
src                                              └┘    └──────────┘      └──────────┘
typ                                              └┘    └──────────┘     └──────────┘ 
doc                                              └┘    └──────────┘       └──────────┘
275  imp_not_comm.mp not_infinite_pos_of_infinite_neg
id   └──────────┘└─┘ └──────────────────────────────┘
src  └──────────┘└─┘ └──────────────────────────────┘
typ  └──────────┘└─┘ └──────────────────────────────┘
276  
277  lemma infinite_neg_neg_of_infinite_pos {x : ℝ*} : infinite_pos x → infinite_neg (-x) :=
id                                               └┘    └──────────┘    └──────────┘  
src                                              └┘    └──────────┘     └──────────┘  
typ                                              └┘    └──────────┘    └──────────┘  
doc                                              └┘    └──────────┘     └──────────┘
278  λ hp r, neg_lt.mp (hp (-r))
id     └┘   └────┘└─┘  └┘  
src          └────┘└─┘      
typ    └┘   └────┘└─┘  └┘  
279  
280  lemma infinite_pos_neg_of_infinite_neg {x : ℝ*} : infinite_neg x → infinite_pos (-x) :=
id                                               └┘    └──────────┘    └──────────┘  
src                                              └┘    └──────────┘     └──────────┘  
typ                                              └┘    └──────────┘    └──────────┘  
doc                                              └┘    └──────────┘     └──────────┘
281  λ hp r, lt_neg.mp (hp (-r))
id     └┘   └────┘└─┘  └┘  
src          └────┘└─┘      
typ    └┘   └────┘└─┘  └┘  
282  
283  lemma infinite_pos_iff_infinite_neg_neg {x : ℝ*} : infinite_pos x ↔ infinite_neg (-x) :=
id                                                └┘    └──────────┘   └──────────┘  
src                                               └┘    └──────────┘    └──────────┘  
typ                                               └┘    └──────────┘   └──────────┘  
doc                                               └┘    └──────────┘     └──────────┘
284  ⟨ infinite_neg_neg_of_infinite_pos, λ hin, neg_neg x ▸ infinite_pos_neg_of_infinite_neg hin ⟩
id     └──────────────────────────────┘    └─┘  └─────┘   └──────────────────────────────┘ └─┘
src    └──────────────────────────────┘         └─────┘    └──────────────────────────────┘
typ    └──────────────────────────────┘    └─┘  └─────┘   └──────────────────────────────┘ └─┘
285  
286  lemma infinite_neg_iff_infinite_pos_neg {x : ℝ*} : infinite_neg x ↔ infinite_pos (-x) :=
id                                                └┘    └──────────┘   └──────────┘  
src                                               └┘    └──────────┘    └──────────┘  
typ                                               └┘    └──────────┘   └──────────┘  
doc                                               └┘    └──────────┘     └──────────┘
287  ⟨ infinite_pos_neg_of_infinite_neg, λ hin, neg_neg x ▸ infinite_neg_neg_of_infinite_pos hin ⟩
id     └──────────────────────────────┘    └─┘  └─────┘   └──────────────────────────────┘ └─┘
src    └──────────────────────────────┘         └─────┘    └──────────────────────────────┘
typ    └──────────────────────────────┘    └─┘  └─────┘   └──────────────────────────────┘ └─┘
288  
289  lemma infinite_iff_infinite_neg {x : ℝ*} : infinite x ↔ infinite (-x) :=
id                                        └┘    └──────┘   └──────┘  
src                                       └┘    └──────┘    └──────┘  
typ                                       └┘    └──────┘   └──────┘  
doc                                       └┘    └──────┘     └──────┘
290  ⟨ λ hi, or.cases_on hi
id       └┘  └─────────┘ └┘
src          └─────────┘
typ      └┘  └─────────┘ └┘
291    (λ hip, or.inr (infinite_neg_neg_of_infinite_pos hip))
id        └─┘  └────┘  └──────────────────────────────┘ └─┘
src            └────┘  └──────────────────────────────┘
typ       └─┘  └────┘  └──────────────────────────────┘ └─┘
292    (λ hin, or.inl (infinite_pos_neg_of_infinite_neg hin)),
id        └─┘  └────┘  └──────────────────────────────┘ └─┘
src            └────┘  └──────────────────────────────┘
typ       └─┘  └────┘  └──────────────────────────────┘ └─┘
293   λ hi, or.cases_on hi
id      └┘  └─────────┘ └┘
src         └─────────┘
typ     └┘  └─────────┘ └┘
294    (λ hipn, or.inr (infinite_neg_iff_infinite_pos_neg.mpr hipn))
id        └──┘  └────┘  └───────────────────────────────┘└──┘ └──┘
src             └────┘  └───────────────────────────────┘└──┘
typ       └──┘  └────┘  └───────────────────────────────┘└──┘ └──┘
295    (λ hinp, or.inl (infinite_pos_iff_infinite_neg_neg.mpr hinp))⟩
id        └──┘  └────┘  └───────────────────────────────┘└──┘ └──┘
src             └────┘  └───────────────────────────────┘└──┘
typ       └──┘  └────┘  └───────────────────────────────┘└──┘ └──┘
296  
297  lemma not_infinite_of_infinitesimal {x : ℝ*} : infinitesimal x → ¬ infinite x :=
id                                            └┘    └───────────┘     └──────┘ 
src                                           └┘    └───────────┘      └──────┘
typ                                           └┘    └───────────┘     └──────┘ 
doc                                           └┘    └───────────┘       └──────┘
298  λ hi hI, have hi' : _ := (hi 2 two_pos), or.dcases_on hI
id     └┘ └┘                   └┘   └─────┘   └──────────┘ └┘
src                                 └─────┘   └──────────┘
typ    └┘ └┘                   └┘   └─────┘   └──────────┘ └┘
299    (λ hip, have hip' : _ := hip 2, not_lt_of_lt hip' (by convert hi'.2; exact (zero_add 2).symm))
id        └─┘                   └─┘    └──────────┘ └──┘             └─┘           └──────┘
src                                    └──────────┘          └──────┘   └┘  └────┘ └──────┘└──────┘
typ       └─┘                   └─┘    └──────────┘ └──┘     └──────┘└─┘└┘  └────┘ └──────┘└──────┘
doc                                                          └──────┘   └┘  └────┘         └──────┘
txt                                                          └──────┘   └┘  └────┘         └──────┘
par                                                          └──────┘   └┘  └────┘         └──────┘
pid                                                                    └┘                └─────┘
st                                                          └─────────────────────────────────────┘
300    (λ hin, have hin' : _ := hin (-2), not_lt_of_lt hin' (by convert hi'.1; exact (zero_sub 2).symm))
id        └─┘                   └─┘      └──────────┘ └──┘             └─┘           └──────┘
src                                      └──────────┘          └──────┘   └┘  └────┘ └──────┘└──────┘
typ       └─┘                   └─┘      └──────────┘ └──┘     └──────┘└─┘└┘  └────┘ └──────┘└──────┘
doc                                                             └──────┘   └┘  └────┘         └──────┘
txt                                                             └──────┘   └┘  └────┘         └──────┘
par                                                             └──────┘   └┘  └────┘         └──────┘
pid                                                                       └┘                └─────┘
st                                                             └─────────────────────────────────────┘
301  
302  lemma not_infinitesimal_of_infinite {x : ℝ*} : infinite x → ¬ infinitesimal x :=
id                                            └┘    └──────┘     └───────────┘ 
src                                           └┘    └──────┘      └───────────┘
typ                                           └┘    └──────┘     └───────────┘ 
doc                                           └┘    └──────┘       └───────────┘
303  imp_not_comm.mp not_infinite_of_infinitesimal
id   └──────────┘└─┘ └───────────────────────────┘
src  └──────────┘└─┘ └───────────────────────────┘
typ  └──────────┘└─┘ └───────────────────────────┘
304  
305  lemma not_infinitesimal_of_infinite_pos {x : ℝ*} : infinite_pos x → ¬ infinitesimal x :=
id                                                └┘    └──────────┘     └───────────┘ 
src                                               └┘    └──────────┘      └───────────┘
typ                                               └┘    └──────────┘     └───────────┘ 
doc                                               └┘    └──────────┘       └───────────┘
306  λ hp, not_infinitesimal_of_infinite (or.inl hp)
id     └┘  └───────────────────────────┘  └────┘ └┘
src        └───────────────────────────┘  └────┘
typ    └┘  └───────────────────────────┘  └────┘ └┘
307  
308  lemma not_infinitesimal_of_infinite_neg {x : ℝ*} : infinite_neg x → ¬ infinitesimal x :=
id                                                └┘    └──────────┘     └───────────┘ 
src                                               └┘    └──────────┘      └───────────┘
typ                                               └┘    └──────────┘     └───────────┘ 
doc                                               └┘    └──────────┘       └───────────┘
309  λ hn, not_infinitesimal_of_infinite (or.inr hn)
id     └┘  └───────────────────────────┘  └────┘ └┘
src        └───────────────────────────┘  └────┘
typ    └┘  └───────────────────────────┘  └────┘ └┘
310  
311  lemma infinite_pos_iff_infinite_and_pos {x : ℝ*} : infinite_pos x ↔ (infinite x ∧ x > 0) :=
id                                                └┘    └──────────┘    └──────┘    
src                                               └┘    └──────────┘     └──────┘      
typ                                               └┘    └──────────┘    └──────┘    
doc                                               └┘    └──────────┘      └──────┘
312  ⟨ λ hip, ⟨or.inl hip, hip 0⟩,
id       └─┘   └────┘ └─┘  └─┘
src            └────┘
typ      └─┘   └────┘ └─┘  └─┘
313    λ ⟨hi, hp⟩, hi.cases_on (λ hip, hip) (λ hin, false.elim (not_lt_of_lt hp (hin 0))) ⟩
id       └┘  └┘     └───────┘    └─┘  └─┘     └─┘  └────────┘  └──────────┘     └─┘
src                  └───────┘                      └────────┘  └──────────┘
typ      └┘  └┘     └───────┘    └─┘  └─┘     └─┘  └────────┘  └──────────┘     └─┘
314  
315  lemma infinite_neg_iff_infinite_and_neg {x : ℝ*} : infinite_neg x ↔ (infinite x ∧ x < 0) :=
id                                                └┘    └──────────┘    └──────┘    
src                                               └┘    └──────────┘     └──────┘      
typ                                               └┘    └──────────┘    └──────┘    
doc                                               └┘    └──────────┘      └──────┘
316  ⟨ λ hip, ⟨or.inr hip, hip 0⟩,
id       └─┘   └────┘ └─┘  └─┘
src            └────┘
typ      └─┘   └────┘ └─┘  └─┘
317    λ ⟨hi, hp⟩, hi.cases_on (λ hin, false.elim (not_lt_of_lt hp (hin 0))) (λ hip, hip) ⟩
id       └┘  └┘     └───────┘    └─┘  └────────┘  └──────────┘     └─┘         └─┘  └─┘
src                  └───────┘         └────────┘  └──────────┘
typ      └┘  └┘     └───────┘    └─┘  └────────┘  └──────────┘     └─┘         └─┘  └─┘
318  
319  lemma infinite_pos_iff_infinite_of_pos {x : ℝ*} (hp : x > 0) : infinite_pos x ↔ infinite x :=
id                                               └┘               └──────────┘   └──────┘ 
src                                              └┘                └──────────┘    └──────┘
typ                                              └┘               └──────────┘   └──────┘ 
doc                                              └┘                 └──────────┘     └──────┘
320  by rw [infinite_pos_iff_infinite_and_pos]; exact ⟨λ hI, hI.1, λ hI, ⟨hI, hp⟩⟩
id          └───────────────────────────────┘                                 └┘
src     └──┘└───────────────────────────────┘  └────┘  └───┘  └──┘ └───┘   └┘  └──
typ     └──┘└───────────────────────────────┘  └────┘  └───┘  └──┘ └───┘   └┘└┘└──
doc     └──┘                                   └────┘  └───┘  └──┘ └───┘   └┘  └──
txt     └──┘                                   └────┘  └───┘  └──┘ └───┘   └┘  └──
par     └──┘                                   └────┘  └───┘  └──┘ └───┘   └┘  └──
pid       └┘                                          └───┘  └──┘ └───┘   └┘  └┘
st     └────────────────────────────────────┘└────────────────────────────────────
321  
src  
typ  
doc  
txt  
par  
pid  
st   
322  lemma infinite_pos_iff_infinite_of_nonneg {x : ℝ*} (hp : x ≥ 0) : infinite_pos x ↔ infinite x :=
id                                                  └┘               └──────────┘   └──────┘ 
src                                                 └┘                └──────────┘    └──────┘
typ                                                 └┘               └──────────┘   └──────┘ 
doc                                                 └┘                 └──────────┘     └──────┘
323  or.cases_on (lt_or_eq_of_le hp) (infinite_pos_iff_infinite_of_pos)
id   └─────────┘  └────────────┘ └┘   └──────────────────────────────┘
src  └─────────┘  └────────────┘      └──────────────────────────────┘
typ  └─────────┘  └────────────┘ └┘   └──────────────────────────────┘
324    (λ h, by rw h.symm; exact
id        
src             └─┘        └─────
typ            └─┘└────┘  └─────
doc             └─┘        └─────
txt             └─┘        └─────
par             └─┘        └─────
pid                            
st             └─────────────────
325    ⟨λ hIP, false.elim (not_infinite_zero (or.inl hIP)), λ hI, false.elim (not_infinite_zero hI)⟩)
id                                            └────┘              └────────┘  └───────────────┘
src  ─┘  └────┘                             └────┘   └──┘ └───┘└────────┘ └───────────────┘  └┘
typ  ─┘  └────┘                             └────┘   └──┘ └───┘└────────┘ └───────────────┘  └┘
doc  ─┘  └────┘                                      └──┘ └───┘                              └┘
txt  ─┘  └────┘                                      └──┘ └───┘                              └┘
par  ─┘  └────┘                                      └──┘ └───┘                              └┘
pid  ─┘  └────┘                                      └──┘ └───┘                              └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘
326  
327  lemma infinite_neg_iff_infinite_of_neg {x : ℝ*} (hn : x < 0) : infinite_neg x ↔ infinite x :=
id                                               └┘               └──────────┘   └──────┘ 
src                                              └┘                └──────────┘    └──────┘
typ                                              └┘               └──────────┘   └──────┘ 
doc                                              └┘                 └──────────┘     └──────┘
328  by rw [infinite_neg_iff_infinite_and_neg]; exact ⟨λ hI, hI.1, λ hI, ⟨hI, hn⟩⟩
id          └───────────────────────────────┘                                 └┘
src     └──┘└───────────────────────────────┘  └────┘  └───┘  └──┘ └───┘   └┘  └──
typ     └──┘└───────────────────────────────┘  └────┘  └───┘  └──┘ └───┘   └┘└┘└──
doc     └──┘                                   └────┘  └───┘  └──┘ └───┘   └┘  └──
txt     └──┘                                   └────┘  └───┘  └──┘ └───┘   └┘  └──
par     └──┘                                   └────┘  └───┘  └──┘ └───┘   └┘  └──
pid       └┘                                          └───┘  └──┘ └───┘   └┘  └┘
st     └────────────────────────────────────┘└────────────────────────────────────
329  
src  
typ  
doc  
txt  
par  
pid  
st   
330  lemma infinite_pos_abs_iff_infinite_abs {x : ℝ*} : infinite_pos (abs x) ↔ infinite (abs x) :=
id                                                └┘    └──────────┘  └─┘    └──────┘  └─┘ 
src                                               └┘    └──────────┘  └─┘     └──────┘  └─┘
typ                                               └┘    └──────────┘  └─┘    └──────┘  └─┘ 
doc                                               └┘    └──────────┘           └──────┘
331  infinite_pos_iff_infinite_of_nonneg (abs_nonneg _)
id   └─────────────────────────────────┘  └────────┘
src  └─────────────────────────────────┘  └────────┘
typ  └─────────────────────────────────┘  └────────┘
332  
333  lemma infinite_iff_infinite_pos_abs {x : ℝ*} : infinite x ↔ infinite_pos (abs x) :=
id                                            └┘    └──────┘   └──────────┘  └─┘ 
src                                           └┘    └──────┘    └──────────┘  └─┘
typ                                           └┘    └──────┘   └──────────┘  └─┘ 
doc                                           └┘    └──────┘     └──────────┘
334  ⟨ λ hi d, or.cases_on hi
id       └┘   └─────────┘ └┘
src            └─────────┘
typ      └┘   └─────────┘ └┘
335     (λ hip, by rw [abs_of_pos (hip 0)]; exact hip d)
id         └─┘         └────────┘  └─┘            └─┘ 
src                └──┘└────────┘    └──┘  └────┘   
typ        └─┘     └──┘└────────┘ └─┘└──┘  └────┘└─┘
doc                └──┘              └──┘  └────┘   
txt                └──┘              └──┘  └────┘   
par                └──┘              └──┘  └────┘   
pid                  └┘              └──┘          
st                └─────────────────────┘└───────────┘
336     (λ hin, by rw [abs_of_neg (hin 0)]; exact lt_neg.mp (hin (-d))),
id         └─┘         └────────┘  └─┘            └───────┘  └─┘  
src                └──┘└────────┘    └──┘  └────┘└───────┘      └┘
typ        └─┘     └──┘└────────┘ └─┘└──┘  └────┘└───────┘ └─┘ └┘
doc                └──┘              └──┘  └────┘                └┘
txt                └──┘              └──┘  └────┘                └┘
par                └──┘              └──┘  └────┘                └┘
pid                  └┘              └──┘                       └┘
st                └─────────────────────┘└──────────────────────────┘
337    λ hipa, by { rcases (lt_trichotomy x 0) with h | h | h,
id       └──┘               └───────────┘ 
src                 └─────┘ └───────────┘ └────────────────┘
typ      └──┘       └─────┘ └───────────┘└────────────────┘
doc                 └─────┘               └────────────────┘
txt                 └─────┘               └────────────────┘
par                 └─────┘               └────────────────┘
pid                                      └────────────────┘
st               └──────────────────────────────────────────┘└─
338      { exact or.inr (infinite_neg_iff_infinite_pos_neg.mpr (by rwa abs_of_neg h at hipa)) },
id               └────┘  └───────────────────────────────────┘         └────────┘ 
src        └────┘└────┘ └───────────────────────────────────┘   └──┘└────────┘ └──────┘└─┘
typ        └────┘└────┘ └───────────────────────────────────┘   └──┘└────────┘└──────┘└─┘
doc        └────┘                                               └──┘           └──────┘└─┘
txt        └────┘                                               └──┘           └──────┘└─┘
par        └────┘                                               └──┘           └──────┘└─┘
pid                                                            └───┘           └────────┘
st   ─────┘└─────────────────────────────────────────────────────┘└───────────────────────┘└─┘└┘
339      { exact false.elim (ne_zero_of_infinite (or.inl (by rw [h]; rwa [h, abs_zero] at hipa)) h) },
id               └────────┘  └─────────────────┘  └────┘                   └──────┘            
src        └────┘└────────┘ └─────────────────┘ └────┘   └──┘ └┘└───┘ └┘└──────┘└───────┘└─┘ └┘
typ        └────┘└────────┘ └─────────────────┘ └────┘   └──┘└┘└───┘└┘└──────┘└───────┘└─┘└┘
doc        └────┘                                        └──┘ └┘└───┘ └┘        └───────┘└─┘ └┘
txt        └────┘                                        └──┘ └┘└───┘ └┘        └───────┘└─┘ └┘
par        └────┘                                        └──┘ └┘└───┘ └┘        └───────┘└─┘ └┘
pid                                                     └───┘ └──────┘ └┘        └──────────┘ 
st   ─────┘└───────────────────────────────────────────────┘└────┘└─────┘└────────┘└──────┘└────┘└┘
340      { exact or.inl (by rwa abs_of_pos h at hipa) } } ⟩
id               └────┘         └────────┘ 
src        └────┘└────┘   └──┘└────────┘ └──────┘└┘
typ        └────┘└────┘   └──┘└────────┘└──────┘└┘
doc        └────┘         └──┘           └──────┘└┘
txt        └────┘         └──┘           └──────┘└┘
par        └────┘         └──┘           └──────┘└┘
pid                      └───┘           └───────┘
st   ─────────────────────┘└───────────────────────┘└┘└──┘
341  
342  lemma infinite_iff_infinite_abs {x : ℝ*} : infinite x ↔ infinite (abs x) :=
id                                        └┘    └──────┘   └──────┘  └─┘ 
src                                       └┘    └──────┘    └──────┘  └─┘
typ                                       └┘    └──────┘   └──────┘  └─┘ 
doc                                       └┘    └──────┘     └──────┘
343  by rw [←infinite_pos_iff_infinite_of_nonneg (abs_nonneg _), infinite_iff_infinite_pos_abs]
id           └─────────────────────────────────┘  └────────┘     └───────────────────────────┘
src     └───┘└─────────────────────────────────┘ └────────┘└───┘└───────────────────────────┘└─
typ     └───┘└─────────────────────────────────┘ └────────┘└───┘└───────────────────────────┘└─
doc     └───┘                                              └───┘                             └─
txt     └───┘                                              └───┘                             └─
par     └───┘                                              └───┘                             └─
pid       └─┘                                              └───┘                             
st     └──────────────────────────────────────────────────────┘└─────────────────────────────┘
344  
src  
typ  
doc  
txt  
par  
pid  
st   
345  lemma infinite_iff_abs_lt_abs {x : ℝ*} : infinite x ↔ ∀ r : ℝ, (abs r : ℝ*) < abs x :=
id                                      └┘    └──────┘            └─┘    └┘   └─┘ 
src                                     └┘    └──────┘             └─┘     └┘   └─┘
typ                                     └┘    └──────┘            └─┘    └┘   └─┘ 
doc                                     └┘    └──────┘                       └┘
346  ⟨ λ hI r, (of_abs U r) ▸ infinite_iff_infinite_pos_abs.mp hI (abs r),
id       └┘    └────┘     └───────────────────────────┘└─┘ └┘  └─┘ 
src             └────┘      └───────────────────────────┘└─┘     └─┘
typ      └┘    └────┘     └───────────────────────────┘└─┘ └┘  └─┘ 
347    λ hR, or.cases_on (max_choice x (-x))
id       └┘  └─────────┘  └────────┘   
src          └─────────┘  └────────┘    
typ      └┘  └─────────┘  └────────┘   
348    (λ h, or.inl $ λ r, lt_of_le_of_lt (le_abs_self _) (h ▸ (hR r)))
id          └────┘       └────────────┘  └─────────┘        └┘ 
src          └────┘        └────────────┘  └─────────┘       
typ         └────┘       └────────────┘  └─────────┘        └┘ 
349    (λ h, or.inr $ λ r, neg_lt_neg_iff.mp $ lt_of_le_of_lt (neg_le_abs_self _) (h ▸ (hR r)))⟩
id          └────┘       └────────────┘└─┘   └────────────┘  └─────────────┘        └┘ 
src          └────┘        └────────────┘└─┘   └────────────┘  └─────────────┘       
typ         └────┘       └────────────┘└─┘   └────────────┘  └─────────────┘        └┘ 
350  
351  lemma infinite_pos_add_not_infinite_neg {x y : ℝ*} :
id                                                  └┘
src                                                 └┘
typ                                                 └┘
doc                                                 └┘
352    infinite_pos x → ¬ infinite_neg y → infinite_pos (x + y) :=
id     └──────────┘     └──────────┘    └──────────┘    
src    └──────────┘      └──────────┘     └──────────┘    
typ    └──────────┘     └──────────┘    └──────────┘    
doc    └──────────┘       └──────────┘     └──────────┘
353  begin
st   └─────
354    intros hip hnin r,
src    └───────────────┘
typ    └───────────────┘
doc    └───────────────┘
txt    └───────────────┘
par    └───────────────┘
pid          └─────────┘
st   ──────────────────┘└─
355    cases not_forall.mp hnin with r₂ hr₂,
id           └───────────┘ └──┘
src    └────┘└───────────┘    └──────────┘
typ    └────┘└───────────┘└──┘└──────────┘
doc    └────┘                 └──────────┘
txt    └────┘                 └──────────┘
par    └────┘                 └──────────┘
pid                          └──────────┘
st   ─────────────────────────────────────┘└─
356    convert (add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂)),
id              └────────────────────┘  └─┘    └┘    └───────┘ └─┘
src    └──────┘ └────────────────────┘        └─┘ └───────┘   └┘
typ    └──────┘ └────────────────────┘ └─┘ └┘└─┘ └───────┘└─┘└┘
doc    └──────┘                                 └─┘             └┘
txt    └──────┘                                 └─┘             └┘
par    └──────┘                                 └─┘             └┘
pid                                            └─┘             └┘
st   ─────────────────────────────────────────────────────────────────┘└─
357    rw [←of_eq_coe, ←of_eq_coe, ←of_eq_coe, of_add, of_neg, ←sub_eq_add_neg, sub_add_cancel]
id          └───────┘   └───────┘   └───────┘  └────┘  └────┘   └────────────┘  └────────────┘
src    └───┘└───────┘└─┘└───────┘└─┘└───────┘└┘└────┘└┘└────┘└─┘└────────────┘└┘└────────────┘└┘
typ    └───┘└───────┘└─┘└───────┘└─┘└───────┘└┘└────┘└┘└────┘└─┘└────────────┘└┘└────────────┘└┘
doc    └───┘         └─┘         └─┘         └┘      └┘      └─┘              └┘              └┘
txt    └───┘         └─┘         └─┘         └┘      └┘      └─┘              └┘              └┘
par    └───┘         └─┘         └─┘         └┘      └┘      └─┘              └┘              └┘
pid      └─┘         └─┘         └─┘         └┘      └┘      └─┘              └┘              
st   ───────────────┘└──────────┘└──────────┘└──────┘└──────┘└───────────────┘└──────────────┘
358  end
st   └─┘
359  
360  lemma not_infinite_neg_add_infinite_pos {x y : ℝ*} :
id                                                  └┘
src                                                 └┘
typ                                                 └┘
doc                                                 └┘
361    ¬ infinite_neg x → infinite_pos y → infinite_pos (x + y) :=
id      └──────────┘    └──────────┘    └──────────┘    
src     └──────────┘     └──────────┘     └──────────┘    
typ     └──────────┘    └──────────┘    └──────────┘    
doc      └──────────┘     └──────────┘     └──────────┘
362  λ hx hy, by rw [add_comm]; exact infinite_pos_add_not_infinite_neg hy hx
id     └┘ └┘         └──────┘         └───────────────────────────────┘ └┘ └┘
src              └──┘└──────┘  └────┘└───────────────────────────────┘    
typ    └┘ └┘     └──┘└──────┘  └────┘└───────────────────────────────┘└┘└┘
doc              └──┘          └────┘                                     
txt              └──┘          └────┘                                     
par              └──┘          └────┘                                     
pid                └┘                                                    
st              └───────────┘└───────────────────────────────────────────────
363  
src  
typ  
doc  
txt  
par  
pid  
st   
364  lemma infinite_neg_add_not_infinite_pos {x y : ℝ*} :
id                                                  └┘
src                                                 └┘
typ                                                 └┘
doc                                                 └┘
365    infinite_neg x → ¬ infinite_pos y → infinite_neg (x + y) :=
id     └──────────┘     └──────────┘    └──────────┘    
src    └──────────┘      └──────────┘     └──────────┘    
typ    └──────────┘     └──────────┘    └──────────┘    
doc    └──────────┘       └──────────┘     └──────────┘
366  by rw [@infinite_neg_iff_infinite_pos_neg x, @infinite_pos_iff_infinite_neg_neg y,
id           └───────────────────────────────┘    └───────────────────────────────┘ 
src     └──┘ └───────────────────────────────┘ └┘ └───────────────────────────────┘ └─
typ     └──┘ └───────────────────────────────┘└┘ └───────────────────────────────┘└─
doc     └──┘                                   └┘                                   └─
txt     └──┘                                   └┘                                   └─
par     └──┘                                   └┘                                   └─
pid       └┘                                   └┘                                   └─
st     └───────────────────────────────────────┘└────────────────────────────────────┘└─
367         @infinite_neg_iff_infinite_pos_neg (x + y), neg_add];
id           └───────────────────────────────┘       └─────┘
src  ──────┘ └───────────────────────────────┘   └─┘└─────┘
typ  ──────┘ └───────────────────────────────┘ └─┘└─────┘
doc  ──────┘                                      └─┘       
txt  ──────┘                                      └─┘       
par  ──────┘                                      └─┘       
pid  ──────┘                                      └─┘       
st   ────────────────────────────────────────────────┘└───────┘└─
368  exact infinite_pos_add_not_infinite_neg
id         └───────────────────────────────┘
src  └────┘└───────────────────────────────┘
typ  └────┘└───────────────────────────────┘
doc  └────┘                                 
txt  └────┘                                 
par  └────┘                                 
pid                                        
st   ────────────────────────────────────────
369  
src  
typ  
doc  
txt  
par  
pid  
st   
370  lemma not_infinite_pos_add_infinite_neg {x y : ℝ*} :
id                                                  └┘
src                                                 └┘
typ                                                 └┘
doc                                                 └┘
371    ¬ infinite_pos x → infinite_neg y → infinite_neg (x + y) :=
id      └──────────┘    └──────────┘    └──────────┘    
src     └──────────┘     └──────────┘     └──────────┘    
typ     └──────────┘    └──────────┘    └──────────┘    
doc      └──────────┘     └──────────┘     └──────────┘
372  λ hx hy, by rw [add_comm]; exact infinite_neg_add_not_infinite_pos hy hx
id     └┘ └┘         └──────┘         └───────────────────────────────┘ └┘ └┘
src              └──┘└──────┘  └────┘└───────────────────────────────┘    
typ    └┘ └┘     └──┘└──────┘  └────┘└───────────────────────────────┘└┘└┘
doc              └──┘          └────┘                                     
txt              └──┘          └────┘                                     
par              └──┘          └────┘                                     
pid                └┘                                                    
st              └───────────┘└───────────────────────────────────────────────
373  
src  
typ  
doc  
txt  
par  
pid  
st   
374  lemma infinite_pos_add_infinite_pos {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
375    infinite_pos x → infinite_pos y → infinite_pos (x + y) :=
id     └──────────┘    └──────────┘    └──────────┘    
src    └──────────┘     └──────────┘     └──────────┘    
typ    └──────────┘    └──────────┘    └──────────┘    
doc    └──────────┘     └──────────┘     └──────────┘
376  λ hx hy, infinite_pos_add_not_infinite_neg hx (not_infinite_neg_of_infinite_pos hy)
id     └┘ └┘  └───────────────────────────────┘ └┘  └──────────────────────────────┘ └┘
src           └───────────────────────────────┘     └──────────────────────────────┘
typ    └┘ └┘  └───────────────────────────────┘ └┘  └──────────────────────────────┘ └┘
377  
378  lemma infinite_neg_add_infinite_neg {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
379    infinite_neg x → infinite_neg y → infinite_neg (x + y) :=
id     └──────────┘    └──────────┘    └──────────┘    
src    └──────────┘     └──────────┘     └──────────┘    
typ    └──────────┘    └──────────┘    └──────────┘    
doc    └──────────┘     └──────────┘     └──────────┘
380  λ hx hy, infinite_neg_add_not_infinite_pos hx (not_infinite_pos_of_infinite_neg hy)
id     └┘ └┘  └───────────────────────────────┘ └┘  └──────────────────────────────┘ └┘
src           └───────────────────────────────┘     └──────────────────────────────┘
typ    └┘ └┘  └───────────────────────────────┘ └┘  └──────────────────────────────┘ └┘
381  
382  lemma infinite_pos_add_not_infinite {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
383    infinite_pos x → ¬ infinite y → infinite_pos (x + y) :=
id     └──────────┘     └──────┘    └──────────┘    
src    └──────────┘      └──────┘     └──────────┘    
typ    └──────────┘     └──────┘    └──────────┘    
doc    └──────────┘       └──────┘     └──────────┘
384  λ hx hy, infinite_pos_add_not_infinite_neg hx (not_or_distrib.mp hy).2
id     └┘ └┘  └───────────────────────────────┘ └┘  └────────────┘└─┘ └┘ 
src           └───────────────────────────────┘     └────────────┘└─┘    
typ    └┘ └┘  └───────────────────────────────┘ └┘  └────────────┘└─┘ └┘ 
385  
386  lemma infinite_neg_add_not_infinite {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
387    infinite_neg x → ¬ infinite y → infinite_neg (x + y) :=
id     └──────────┘     └──────┘    └──────────┘    
src    └──────────┘      └──────┘     └──────────┘    
typ    └──────────┘     └──────┘    └──────────┘    
doc    └──────────┘       └──────┘     └──────────┘
388  λ hx hy, infinite_neg_add_not_infinite_pos hx (not_or_distrib.mp hy).1
id     └┘ └┘  └───────────────────────────────┘ └┘  └────────────┘└─┘ └┘ 
src           └───────────────────────────────┘     └────────────┘└─┘    
typ    └┘ └┘  └───────────────────────────────┘ └┘  └────────────┘└─┘ └┘ 
389  
390  theorem infinite_pos_of_tendsto_top {f : ℕ → ℝ} (hf : tendsto f at_top at_top) :
id                                                       └─────┘  └────┘ └────┘
src                                                      └─────┘   └────┘ └────┘
typ                                                      └─────┘  └────┘ └────┘
doc                                                        └─────┘   └────┘ └────┘
391    infinite_pos (of_seq f) :=
id     └──────────┘  └────┘ 
src    └──────────┘  └────┘
typ    └──────────┘  └────┘ 
doc    └──────────┘
392  λ r, have hf' : _ := (tendsto_at_top_at_top _).mp hf,
id                        └───────────────────┘   └┘  └┘
src                        └───────────────────┘   └┘
typ                       └───────────────────┘   └┘  └┘
393  Exists.cases_on (hf' (r + 1)) $ λ i hi,
id   └─────────────┘  └─┘             └┘
src  └─────────────┘         
typ  └─────────────┘  └─┘             └┘
394    have hi' : ∀ (a : ℕ), f a < (r + 1) → a < i :=
id                                       
src                                         
typ                                      
395      λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
id                   └────┘   └────┘         └─────────────┘  └┘ 
src              └───┘└────┘└─┘└────┘  └────┘└─────────────┘    
typ             └───┘└────┘└─┘└────┘  └────┘└─────────────┘ └┘
doc              └───┘      └─┘        └────┘                   
txt              └───┘      └─┘        └────┘                   
par              └───┘      └─┘        └────┘                   
pid                └─┘      └─┘                                
st              └──────────┘└───────┘└────────────────────────────┘
396    have hS : - {a : ℕ | r < f a} ⊆ {a : ℕ | a ≤ i} :=
id                                      
src                                        
typ                                     
397      by simp only [set.compl_set_of, not_lt];
id                     └──────────────┘  └────┘
src         └─────────┘└──────────────┘└┘└────┘
typ         └─────────┘└──────────────┘└┘└────┘
doc         └─────────┘                └┘      
txt         └─────────┘                └┘      
par         └─────────┘                └┘      
pid             └──┘└┘                └┘      
st         └──────────────────────────────────────
398      exact λ a har, le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _))),
id                      └──────┘  └─┘    └────────────┘      └────────┘
src      └────┘ └──────┘└──────┘      └────────────┘    └────────┘└───┘
typ      └────┘ └──────┘└──────┘ └─┘  └────────────┘    └────────┘└───┘
doc      └────┘ └──────┘                                          └───┘
txt      └────┘ └──────┘                                          └───┘
par      └────┘ └──────┘                                          └───┘
pid            └──────┘                                          └───┘
st   ──────────────────────────────────────────────────────────────────────┘
399    (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
id      └────┘  └─┘    └─────────────────────────────┘
src     └────┘  └─┘    └─────────────────────────────┘
typ     └────┘  └─┘    └─────────────────────────────┘
400    set.finite_subset (set.finite_le_nat _) hS
id     └───────────────┘  └───────────────┘    └┘
src    └───────────────┘  └───────────────┘
typ    └───────────────┘  └───────────────┘    └┘
401  
402  theorem infinite_neg_of_tendsto_bot {f : ℕ → ℝ} (hf : tendsto f at_top at_bot) :
id                                                       └─────┘  └────┘ └────┘
src                                                      └─────┘   └────┘ └────┘
typ                                                      └─────┘  └────┘ └────┘
doc                                                        └─────┘   └────┘ └────┘
403    infinite_neg (of_seq f) :=
id     └──────────┘  └────┘ 
src    └──────────┘  └────┘
typ    └──────────┘  └────┘ 
doc    └──────────┘
404  λ r, have hf' : _ := (tendsto_at_top_at_bot _).mp hf,
id                        └───────────────────┘   └┘  └┘
src                        └───────────────────┘   └┘
typ                       └───────────────────┘   └┘  └┘
405  Exists.cases_on (hf' (r - 1)) $ λ i hi,
id   └─────────────┘  └─┘             └┘
src  └─────────────┘         
typ  └─────────────┘  └─┘             └┘
406    have hi' : ∀ (a : ℕ), r - 1 < f a → a < i :=
id                                     
src                                       
typ                                    
407      λ a, by rw [←not_le, ←not_le]; exact not_imp_not.mpr (hi a),
id                   └────┘   └────┘         └─────────────┘  └┘ 
src              └───┘└────┘└─┘└────┘  └────┘└─────────────┘    
typ             └───┘└────┘└─┘└────┘  └────┘└─────────────┘ └┘
doc              └───┘      └─┘        └────┘                   
txt              └───┘      └─┘        └────┘                   
par              └───┘      └─┘        └────┘                   
pid                └─┘      └─┘                                
st              └──────────┘└───────┘└────────────────────────────┘
408    have hS : - {a : ℕ | f a < r} ⊆ {a : ℕ | a ≤ i} :=
id                                      
src                                        
typ                                     
409      by simp only [set.compl_set_of, not_lt];
id                     └──────────────┘  └────┘
src         └─────────┘└──────────────┘└┘└────┘
typ         └─────────┘└──────────────┘└┘└────┘
doc         └─────────┘                └┘      
txt         └─────────┘                └┘      
par         └─────────┘                └┘      
pid             └──┘└┘                └┘      
st         └──────────────────────────────────────
410      exact λ a har, le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har)),
id                      └──────┘  └─┘    └────────────┘  └────────┘
src      └────┘ └──────┘└──────┘      └────────────┘ └────────┘└──┘   └┘
typ      └────┘ └──────┘└──────┘ └─┘  └────────────┘ └────────┘└──┘   └┘
doc      └────┘ └──────┘                                       └──┘   └┘
txt      └────┘ └──────┘                                       └──┘   └┘
par      └────┘ └──────┘                                       └──┘   └┘
pid            └──────┘                                       └──┘   └┘
st   ──────────────────────────────────────────────────────────────────────┘
411    (lt_def U).mpr $ mem_hyperfilter_of_finite_compl $
id      └────┘  └─┘    └─────────────────────────────┘
src     └────┘  └─┘    └─────────────────────────────┘
typ     └────┘  └─┘    └─────────────────────────────┘
412    set.finite_subset (set.finite_le_nat _) hS
id     └───────────────┘  └───────────────┘    └┘
src    └───────────────┘  └───────────────┘
typ    └───────────────┘  └───────────────┘    └┘
413  
414  lemma not_infinite_neg {x : ℝ*} : ¬ infinite x → ¬ infinite (-x) :=
id                               └┘     └──────┘     └──────┘  
src                              └┘     └──────┘      └──────┘  
typ                              └┘     └──────┘     └──────┘  
doc                              └┘      └──────┘       └──────┘
415  not_imp_not.mpr infinite_iff_infinite_neg.mpr
id   └─────────┘└──┘ └───────────────────────┘└──┘
src  └─────────┘└──┘ └───────────────────────┘└──┘
typ  └─────────┘└──┘ └───────────────────────┘└──┘
416  
417  lemma not_infinite_add {x y : ℝ*} (hx : ¬ infinite x) (hy : ¬ infinite y) :
id                                 └┘         └──────┘          └──────┘ 
src                                └┘         └──────┘           └──────┘
typ                                └┘         └──────┘          └──────┘ 
doc                                └┘          └──────┘            └──────┘
418    ¬ infinite (x + y) :=
id      └──────┘    
src     └──────┘    
typ     └──────┘    
doc      └──────┘
419  have hx' : _ := exists_st_of_not_infinite hx, have hy' : _ := exists_st_of_not_infinite hy,
id                   └───────────────────────┘ └┘                  └───────────────────────┘ └┘
src                  └───────────────────────┘                     └───────────────────────┘
typ                  └───────────────────────┘ └┘                  └───────────────────────┘ └┘
420  Exists.cases_on hx' $ Exists.cases_on hy' $
id   └─────────────┘ └─┘   └─────────────┘ └─┘
src  └─────────────┘       └─────────────┘
typ  └─────────────┘ └─┘   └─────────────┘ └─┘
421  λ r hr s hs, not_infinite_of_exists_st $ ⟨s + r, is_st_add hs hr⟩
id      └┘  └┘  └───────────────────────┘        └───────┘ └┘ └┘
src               └───────────────────────┘          └───────┘
typ     └┘  └┘  └───────────────────────┘        └───────┘ └┘ └┘
422  
423  theorem not_infinite_iff_exist_lt_gt {x : ℝ*} : ¬ infinite x ↔ ∃ r s : ℝ, (r : ℝ*) < x ∧ x < s :=
id                                             └┘     └──────┘               └┘       
src                                            └┘     └──────┘                 └┘        
typ                                            └┘     └──────┘               └┘       
doc                                            └┘      └──────┘                     └┘
424  ⟨ λ hni,
id       └─┘
typ      └─┘
425  Exists.dcases_on (not_forall.mp (not_or_distrib.mp hni).1) $
id   └──────────────┘  └────────┘└─┘  └────────────┘└─┘ └─┘ 
src  └──────────────┘  └────────┘└─┘  └────────────┘└─┘     
typ  └──────────────┘  └────────┘└─┘  └────────────┘└─┘ └─┘ 
426  Exists.dcases_on (not_forall.mp (not_or_distrib.mp hni).2) $ λ r hr s hs,
id   └──────────────┘  └────────┘└─┘  └────────────┘└─┘ └─┘         └┘  └┘
src  └──────────────┘  └────────┘└─┘  └────────────┘└─┘     
typ  └──────────────┘  └────────┘└─┘  └────────────┘└─┘ └─┘         └┘  └┘
427  by rw [not_lt] at hr hs; exact ⟨r - 1, s + 1,
id          └────┘                         
src     └──┘└────┘└────────┘  └────┘  └──┘ └───
typ     └──┘└────┘└────────┘  └────┘ └──┘└───
doc     └──┘      └────────┘  └────┘   └──┘  └───
txt     └──┘      └────────┘  └────┘   └──┘  └───
par     └──┘      └────────┘  └────┘   └──┘  └───
pid       └┘      └───────┘          └──┘  └───
st     └─────────┘└───────────────────────────────
428    ⟨ lt_of_lt_of_le (by rw [←of_eq_coe, of_sub]; exact sub_one_lt _) hr,
id       └────────────┘          └───────┘  └────┘         └────────┘    └┘
src  ─┘ └────────────┘   └───┘└───────┘└┘└────┘└──────┘└────────┘└──┘  └─
typ  ─┘ └────────────┘   └───┘└───────┘└┘└────┘└──────┘└────────┘└──┘└┘└─
doc  ─┘                  └───┘         └┘      └──────┘          └──┘  └─
txt  ─┘                  └───┘         └┘      └──────┘          └──┘  └─
par  ─┘                  └───┘         └┘      └──────┘          └──┘  └─
pid  ─┘                  └────┘         └┘      └───────┘          └──┘  └─
st   ─────────────────────┘└─────────────┘└──────┘└──────────────────┘└─────
429      lt_of_le_of_lt hs (by rw [←of_eq_coe (s + 1), of_add]; exact lt_add_one _)⟩ ⟩,
id       └────────────┘ └┘          └───────┘         └────┘         └────────┘
src  ───┘└────────────┘     └───┘└───────┘   └───┘└────┘└──────┘└────────┘└────┘
typ  ───┘└────────────┘└┘   └───┘└───────┘  └───┘└────┘└──────┘└────────┘└────┘
doc  ───┘                   └───┘            └───┘      └──────┘          └────┘
txt  ───┘                   └───┘            └───┘      └──────┘          └────┘
par  ───┘                   └───┘            └───┘      └──────┘          └────┘
pid  ───┘                   └────┘            └───┘      └───────┘          └────┘
st   ────────────────────────┘└─────────────────────┘└──────┘└──────────────────┘└──┘
430  λ hrs, Exists.dcases_on hrs $ λ r hr, Exists.dcases_on hr $ λ s hs,
id     └─┘  └──────────────┘ └─┘      └┘  └──────────────┘ └┘      └┘
src         └──────────────┘               └──────────────┘
typ    └─┘  └──────────────┘ └─┘      └┘  └──────────────┘ └┘      └┘
431    not_or_distrib.mpr ⟨not_forall.mpr ⟨s, lt_asymm (hs.2)⟩, not_forall.mpr ⟨r, lt_asymm (hs.1) ⟩⟩⟩
id     └────────────┘└──┘  └────────┘└──┘    └──────┘  └┘     └────────┘└──┘    └──────┘  └┘
src    └────────────┘└──┘  └────────┘└──┘     └──────┘         └────────┘└──┘     └──────┘    
typ    └────────────┘└──┘  └────────┘└──┘    └──────┘  └┘     └────────┘└──┘    └──────┘  └┘
432  
433  theorem not_infinite_real (r : ℝ) : ¬ infinite r := by rw not_infinite_iff_exist_lt_gt; exact
id                                       └──────┘           └──────────────────────────┘
src                                      └──────┘         └─┘└──────────────────────────┘  └────┘
typ                                      └──────┘        └─┘└──────────────────────────┘  └────┘
doc                                        └──────┘         └─┘                              └────┘
txt                                                         └─┘                              └────┘
par                                                         └─┘                              └────┘
pid                                                                                              
st                                                         └───────────────────────────────────────
434  ⟨ r - 1, r + 1,
id            
src    └──┘ └───
typ    └──┘└───
doc     └──┘  └───
txt     └──┘  └───
par     └──┘  └───
pid     └──┘  └───
st   ────────────────
435    by rw [←of_eq_coe, ←of_eq_coe, ←of_lt U]; exact sub_one_lt _,
id             └───────┘   └───────┘   └───┘          └────────┘
src  ─┘  └───┘└───────┘└─┘└───────┘└─┘└───┘└──────┘└────────┘└───
typ  ─┘  └───┘└───────┘└─┘└───────┘└─┘└───┘└──────┘└────────┘└───
doc  ─┘  └───┘         └─┘         └─┘      └──────┘          └───
txt  ─┘  └───┘         └─┘         └─┘      └──────┘          └───
par  ─┘  └───┘         └─┘         └─┘      └──────┘          └───
pid  ─┘  └────┘         └─┘         └─┘      └───────┘          └───
st   ───┘└─────────────┘└──────────┘└────────┘└──────────────────┘└─
436    by rw [←of_eq_coe, ←of_eq_coe, ←of_lt U]; exact lt_add_one _⟩
id             └───────┘   └───────┘   └───┘          └────────┘
src  ─┘  └───┘└───────┘└─┘└───────┘└─┘└───┘└──────┘└────────┘└───
typ  ─┘  └───┘└───────┘└─┘└───────┘└─┘└───┘└──────┘└────────┘└───
doc  ─┘  └───┘         └─┘         └─┘      └──────┘          └───
txt  ─┘  └───┘         └─┘         └─┘      └──────┘          └───
par  ─┘  └───┘         └─┘         └─┘      └──────┘          └───
pid  ─┘  └────┘         └─┘         └─┘      └───────┘          └─┘
st   ───┘└─────────────┘└──────────┘└────────┘└──────────────────┘└─
437  
src  
typ  
doc  
txt  
par  
pid  
st   
438  theorem not_real_of_infinite {x : ℝ*} : infinite x → ∀ r : ℝ, x ≠ of r :=
id                                     └┘    └──────┘              └┘ 
src                                    └┘    └──────┘                └┘
typ                                    └┘    └──────┘              └┘ 
doc                                    └┘    └──────┘                  └┘
439  λ hi r hr,  not_infinite_real r $ @eq.subst _ infinite _ _ hr hi
id     └┘  └┘   └───────────────┘     └──────┘   └──────┘     └┘ └┘
src              └───────────────┘      └──────┘   └──────┘
typ    └┘  └┘   └───────────────┘     └──────┘   └──────┘     └┘ └┘
doc                                                └──────┘
440  
441  -- FACTS ABOUT ST THAT REQUIRE SOME INFINITE MACHINERY
442  
443  private lemma is_st_mul' {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) (hs : s ≠ 0) :
id                                   └┘                  └───┘           └───┘           
src                                  └┘                  └───┘             └───┘              
typ                                  └┘                  └───┘           └───┘           
doc                                  └┘                   └───┘             └───┘
444    is_st (x * y) (r * s) :=
id     └───┘         
src    └───┘           
typ    └───┘         
doc    └───┘
445  have hxr' : _ := is_st_iff_abs_sub_lt_delta.mp hxr,
id                    └────────────────────────┘└─┘ └─┘
src                   └────────────────────────┘└─┘
typ                   └────────────────────────┘└─┘ └─┘
446  have hys' : _ := is_st_iff_abs_sub_lt_delta.mp hys,
id                    └────────────────────────┘└─┘ └─┘
src                   └────────────────────────┘└─┘
typ                   └────────────────────────┘└─┘ └─┘
447  have h : _ := not_infinite_iff_exist_lt_gt.mp $ not_imp_not.mpr infinite_iff_infinite_abs.mpr $
id                 └──────────────────────────┘└─┘   └─────────┘└──┘ └───────────────────────┘└──┘
src                └──────────────────────────┘└─┘   └─────────┘└──┘ └───────────────────────┘└──┘
typ                └──────────────────────────┘└─┘   └─────────┘└──┘ └───────────────────────┘└──┘
448  not_infinite_of_exists_st ⟨r, hxr⟩,
id   └───────────────────────┘    └─┘
src  └───────────────────────┘
typ  └───────────────────────┘    └─┘
449  Exists.cases_on h $ λ u h', Exists.cases_on h' $ λ t ⟨hu, ht⟩,
id   └─────────────┘       └┘  └─────────────┘ └┘          └┘
src  └─────────────┘             └─────────────┘
typ  └─────────────┘       └┘  └─────────────┘ └┘          └┘
450  is_st_iff_abs_sub_lt_delta.mpr $ λ d hd,
id   └────────────────────────┘└──┘      └┘
src  └────────────────────────┘└──┘
typ  └────────────────────────┘└──┘      └┘
451     calc abs (x * y - of (r * s))
id           └─┘      └┘    
src          └─┘        └┘    
typ          └─┘      └┘    
doc                       └┘
452        = abs (x * y - (of r) * (of s)) : by rw of_mul
id           └─┘       └┘     └┘            └────┘
src          └─┘         └┘      └┘          └─┘└────┘
typ          └─┘       └┘     └┘         └─┘└────┘
doc                        └┘       └┘          └─┘      
txt                                             └─┘      
par                                             └─┘      
pid                                                     
st                                  └┘         └──────────
453    ... = abs (x * (y - of s) + (x - of r) * (of s)) :
id           └─┘       └┘       └┘     └┘ 
src  ─┘      └─┘         └┘         └┘      └┘
typ  ─┘      └─┘       └┘       └┘     └┘ 
doc  ─┘                    └┘           └┘       └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
454          by rw [mul_sub, sub_mul, add_sub, sub_add_cancel]
id                  └─────┘  └─────┘  └─────┘  └────────────┘
src             └──┘└─────┘└┘└─────┘└┘└─────┘└┘└────────────┘└─
typ             └──┘└─────┘└┘└─────┘└┘└─────┘└┘└────────────┘└─
doc             └──┘       └┘       └┘       └┘              └─
txt             └──┘       └┘       └┘       └┘              └─
par             └──┘       └┘       └┘       └┘              └─
pid               └┘       └┘       └┘       └┘              
st             └──────────┘└───────┘└───────┘└──────────────┘
455    ... ≤ abs (x * (y - of s)) + abs ((x - of r) * (of s)) : abs_add _ _
id           └─┘       └┘     └─┘     └┘     └┘      └─────┘
src  ─┘      └─┘         └┘      └─┘      └┘      └┘       └─────┘
typ  ─┘      └─┘       └┘     └─┘     └┘     └┘      └─────┘
doc  ─┘                    └┘                 └┘       └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
456    ... ≤ abs x * abs (y - of s) + abs (x - of r) * abs (of s) : by simp only [abs_mul]
id           └─┘   └─┘    └┘    └─┘    └┘    └─┘  └┘                   └─────┘
src          └─┘    └─┘     └┘     └─┘     └┘     └─┘  └┘         └─────────┘└─────┘└─
typ          └─┘   └─┘    └┘    └─┘    └┘    └─┘  └┘        └─────────┘└─────┘└─
doc                           └┘               └┘           └┘         └─────────┘       └─
txt                                                                    └─────────┘       └─
par                                                                    └─────────┘       └─
pid                                                                        └──┘└┘       
st                                                                    └────────────────────
457    ... ≤ abs x * of ((d / t) / 2) + of ((d / abs s) / 2) * abs (of s) : add_le_add
id           └─┘   └┘            └┘     └─┘        └─┘  └┘     └────────┘
src  ─┘      └─┘    └┘              └┘      └─┘         └─┘  └┘      └────────┘
typ  ─┘      └─┘   └┘            └┘     └─┘        └─┘  └┘     └────────┘
doc  ─┘              └┘                 └┘                          └┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘
458          (mul_le_mul_of_nonneg_left (le_of_lt $ hys' _ $ half_pos $ div_pos hd $
id            └───────────────────────┘  └──────┘   └──┘     └──────┘   └─────┘ └┘
src           └───────────────────────┘  └──────┘            └──────┘   └─────┘
typ           └───────────────────────┘  └──────┘   └──┘     └──────┘   └─────┘ └┘
459            (of_lt U).mpr $ lt_of_le_of_lt (abs_nonneg _) ht) $ abs_nonneg _ )
id              └───┘  └─┘    └────────────┘  └────────┘          └────────┘
src             └───┘  └─┘    └────────────┘  └────────┘          └────────┘
typ             └───┘  └─┘    └────────────┘  └────────┘          └────────┘
460          (mul_le_mul_of_nonneg_right (le_of_lt $ hxr' _ $ half_pos $ div_pos hd $
id            └────────────────────────┘  └──────┘   └──┘     └──────┘   └─────┘ └┘
src           └────────────────────────┘  └──────┘            └──────┘   └─────┘
typ           └────────────────────────┘  └──────┘   └──┘     └──────┘   └─────┘ └┘
461            abs_pos_of_ne_zero hs) $ abs_nonneg _)
id             └────────────────┘ └┘    └────────┘
src            └────────────────┘       └────────┘
typ            └────────────────┘ └┘    └────────┘
462    ... = (of d) / 2 * (abs x / of t) + ((of d) / 2) : by
id            └┘        └─┘   └┘      └┘   
src           └┘         └─┘    └┘       └┘    
typ           └┘        └─┘   └┘      └┘   
doc           └┘                   └┘        └┘
st                                                          
463        { rw [div_div_eq_div_mul, mul_comm t 2, ←div_div_eq_div_mul,
id               └────────────────┘  └──────┘      └────────────────┘
src          └──┘└────────────────┘└┘└──────┘ └───┘└────────────────┘└─
typ          └──┘└────────────────┘└┘└──────┘└───┘└────────────────┘└─
doc          └──┘                  └┘         └───┘                  └─
txt          └──┘                  └┘         └───┘                  └─
par          └──┘                  └┘         └───┘                  └─
pid            └┘                  └┘         └───┘                  └─
st   ─────────────────────────────┘└───────────┘└────────────────────┘└─
464              of_div U, div_div_eq_div_mul, mul_comm (abs s) 2,
id               └────┘   └────────────────┘  └──────┘  └─┘ 
src  ───────────┘└────┘└┘└────────────────┘└┘└──────┘ └─┘ └────
typ  ───────────┘└────┘└┘└────────────────┘└┘└──────┘ └─┘└────
doc  ───────────┘       └┘                  └┘             └────
txt  ───────────┘       └┘                  └┘             └────
par  ───────────┘       └┘                  └┘             └────
pid  ───────────┘       └┘                  └┘             └────
st   ───────────────────┘└──────────────────┘└─────────────────┘└──
465          ←div_div_eq_div_mul, mul_div_comm, of_div U, of_div U, of_div U, of_abs U,
id            └────────────────┘  └──────────┘  └────┘   └────┘   └────┘   └────┘ 
src  ────────┘└────────────────┘└┘└──────────┘└┘└────┘└┘└────┘└┘└────┘└┘└────┘└─
typ  ────────┘└────────────────┘└┘└──────────┘└┘└────┘└┘└────┘└┘└────┘└┘└────┘└─
doc  ────────┘                  └┘            └┘       └┘       └┘       └┘       └─
txt  ────────┘                  └┘            └┘       └┘       └┘       └┘       └─
par  ────────┘                  └┘            └┘       └┘       └┘       └┘       └─
pid  ────────┘                  └┘            └┘       └┘       └┘       └┘       └─
st   ──────────────────────────┘└────────────┘└────────┘└────────┘└────────┘└────────┘└─
466          div_mul_cancel _ (ne_of_gt (abs_pos_of_ne_zero ((of_ne_zero U.1 _).mp hs)))], refl }
id           └────────────┘    └──────┘  └────────────────┘   └────────┘          └┘
src  ───────┘└────────────┘└─┘ └──────┘ └────────────────┘  └────────┘└───────┘  └──┘  └───┘
typ  ───────┘└────────────┘└─┘ └──────┘ └────────────────┘  └────────┘└───────┘└┘└──┘  └───┘
doc  ───────┘              └─┘                                         └───────┘  └──┘  └───┘
txt  ───────┘              └─┘                                         └───────┘  └──┘  └───┘
par  ───────┘              └─┘                                         └───────┘  └──┘  └───┘
pid  ───────┘              └─┘                                         └───────┘  └──┘      
st   ──────────────────────────────────────────────────────────────────────────────────┘└──────┘└┘
467    ... < (of d) / 2 * 1 + ((of d) / 2) :
id            └┘            └┘   
src           └┘             └┘    
typ           └┘            └┘   
doc           └┘                └┘
468          add_lt_add_right (mul_lt_mul_of_pos_left
id           └──────────────┘  └────────────────────┘
src          └──────────────┘  └────────────────────┘
typ          └──────────────┘  └────────────────────┘
469          ((div_lt_one_iff_lt $ lt_of_le_of_lt (abs_nonneg x) ht).mpr ht) $
id             └───────────────┘   └────────────┘  └────────┘      └─┘
src            └───────────────┘   └────────────┘  └────────┘       └─┘
typ            └───────────────┘   └────────────┘  └────────┘      └─┘
470          half_pos $ of_lt_of_lt U hd) _
id           └──────┘   └─────────┘  └┘
src          └──────┘   └─────────┘ 
typ          └──────┘   └─────────┘  └┘
471    ... = of d : by rw [mul_one, add_halves]
id           └┘           └─────┘  └────────┘
src          └┘        └──┘└─────┘└┘└────────┘└─
typ          └┘       └──┘└─────┘└┘└────────┘└─
doc          └┘        └──┘       └┘          └─
txt                    └──┘       └┘          └─
par                    └──┘       └┘          └─
pid                      └┘       └┘          
st                    └──────────┘└──────────┘
472  
src  
typ  
doc  
txt  
par  
pid  
st   
473  lemma is_st_mul {x y : ℝ*} {r s : ℝ} (hxr : is_st x r) (hys : is_st y s) :
id                          └┘                  └───┘           └───┘  
src                         └┘                  └───┘             └───┘
typ                         └┘                  └───┘           └───┘  
doc                         └┘                   └───┘             └───┘
474    is_st (x * y) (r * s) :=
id     └───┘         
src    └───┘           
typ    └───┘         
doc    └───┘
475  have h : _ := not_infinite_iff_exist_lt_gt.mp $
id                 └──────────────────────────┘└─┘
src                └──────────────────────────┘└─┘
typ                └──────────────────────────┘└─┘
476    not_imp_not.mpr infinite_iff_infinite_abs.mpr $ not_infinite_of_exists_st ⟨r, hxr⟩,
id     └─────────┘└──┘ └───────────────────────┘└──┘   └───────────────────────┘    └─┘
src    └─────────┘└──┘ └───────────────────────┘└──┘   └───────────────────────┘
typ    └─────────┘└──┘ └───────────────────────┘└──┘   └───────────────────────┘    └─┘
477  Exists.cases_on h $ λ u h', Exists.cases_on h' $ λ t ⟨hu, ht⟩,
id   └─────────────┘       └┘  └─────────────┘ └┘      
src  └─────────────┘             └─────────────┘
typ  └─────────────┘       └┘  └─────────────┘ └┘      
478  begin
st   └─────
479    by_cases hs : s = 0,
id                    
src    └───────┘  └─┘ └┘
typ    └───────┘  └─┘└┘
doc    └───────┘  └─┘  └┘
txt    └───────┘  └─┘  └┘
par    └───────┘  └─┘  └┘
pid              └─┘  
st   ────────────────────┘└─
480    { apply is_st_iff_abs_sub_lt_delta.mpr, intros d hd,
src      └────┘                                └─────────┘
typ      └────┘                                └─────────┘
doc      └────┘                                └─────────┘
txt      └────┘                                └─────────┘
par      └────┘                                └─────────┘
pid                                                 └───┘
st   ───┘└──────────────────────────────────┘└───────────┘└─
481      have hys' : _ := is_st_iff_abs_sub_lt_delta.mp hys (d / t)
id                        └───────────────────────────┘ └─┘    
src      └───────────────┘└───────────────────────────┘      └─
typ      └───────────────┘└───────────────────────────┘└─┘ └─
doc      └───────────────┘                                    └─
txt      └───────────────┘                                    └─
par      └───────────────┘                                    └─
pid      └───────┘└──┘└──┘                                    └─
st   ───────────────────────────────────────────────────────────────
482        (div_pos hd ((of_lt U).mpr (lt_of_le_of_lt (abs_nonneg x) ht))),
id          └─────┘ └┘   └───┘        └────────────┘  └────────┘   └┘
src  ─────┘ └─────┘    └───┘└────┘ └────────────┘ └────────┘ └┘  └─┘
typ  ─────┘ └─────┘└┘  └───┘└────┘ └────────────┘ └────────┘└┘└┘└─┘
doc  ─────┘                  └────┘                           └┘  └─┘
txt  ─────┘                  └────┘                           └┘  └─┘
par  ─────┘                  └────┘                           └┘  └─┘
pid  ─────┘                  └────┘                           └┘  └─┘
st   ────────────────────────────────────────────────────────────────────┘└─
483      rw [hs, ←of_eq_coe _, of_zero, sub_zero] at hys',
id           └┘   └───────┘    └─────┘  └──────┘
src      └──┘  └─┘└───────┘└──┘└─────┘└┘└──────┘└───────┘
typ      └──┘└┘└─┘└───────┘└──┘└─────┘└┘└──────┘└───────┘
doc      └──┘  └─┘         └──┘       └┘        └───────┘
txt      └──┘  └─┘         └──┘       └┘        └───────┘
par      └──┘  └─┘         └──┘       └┘        └───────┘
pid        └┘  └─┘         └──┘       └┘        └──────┘
st   ─────────┘└────────────┘└───────┘└────────┘└──────┘└─
484      rw [hs, mul_zero, (of_eq_coe _).symm, of_zero, sub_zero, abs_mul, mul_comm,
id           └┘  └──────┘   └───────┘          └─────┘  └──────┘  └─────┘  └──────┘
src      └──┘  └┘└──────┘└┘ └───────┘└────────┘└─────┘└┘└──────┘└┘└─────┘└┘└──────┘└─
typ      └──┘└┘└┘└──────┘└┘ └───────┘└────────┘└─────┘└┘└──────┘└┘└─────┘└┘└──────┘└─
doc      └──┘  └┘        └┘          └────────┘       └┘        └┘       └┘        └─
txt      └──┘  └┘        └┘          └────────┘       └┘        └┘       └┘        └─
par      └──┘  └┘        └┘          └────────┘       └┘        └┘       └┘        └─
pid        └┘  └┘        └┘          └────────┘       └┘        └┘       └┘        └─
st   ─────────┘└────────┘└─────────────────┘└────────┘└────────┘└───────┘└────────┘└─
485          ←div_mul_cancel (d : ℝ*) (ne_of_gt (lt_of_le_of_lt (abs_nonneg x) ht)),
id            └────────────┘          └──────┘  └────────────┘  └────────┘   └┘
src  ────────┘└────────────┘  └─┘  └┘ └──────┘ └────────────┘ └────────┘ └┘  └───
typ  ────────┘└────────────┘ └─┘  └┘ └──────┘ └────────────┘ └────────┘└┘└┘└───
doc  ────────┘                └─┘  └┘                                    └┘  └───
txt  ────────┘                └─┘  └┘                                    └┘  └───
par  ────────┘                └─┘  └┘                                    └┘  └───
pid  ────────┘                └─┘  └┘                                    └┘  └───
st   ─────────────────────────────────────────────────────────────────────────────┘└─
486          ←of_eq_coe d, ←of_eq_coe t, ←of_div U],
id            └───────┘    └───────┘    └────┘ 
src  ────────┘└───────┘ └─┘└───────┘ └─┘└────┘
typ  ────────┘└───────┘└─┘└───────┘└─┘└────┘
doc  ────────┘          └─┘          └─┘       
txt  ────────┘          └─┘          └─┘       
par  ────────┘          └─┘          └─┘       
pid  ────────┘          └─┘          └─┘       
st   ───────────────────┘└────────────┘└─────────┘└──
487      exact mul_lt_mul'' hys' ht (abs_nonneg _) (abs_nonneg _) },
id             └──────────┘ └──┘ └┘                 └────────┘
src      └────┘└──────────┘                 └──┘ └────────┘└──┘
typ      └────┘└──────────┘└──┘└┘           └──┘ └────────┘└──┘
doc      └────┘                             └──┘           └──┘
txt      └────┘                             └──┘           └──┘
par      └────┘                             └──┘           └──┘
pid                                        └──┘           └─┘
st   ────────────────────────────────────────────────────────────┘└┘
488    exact is_st_mul' hxr hys hs,
id           └────────┘ └─┘ └─┘ └┘
src    └────┘└────────┘      
typ    └────┘└────────┘└─┘└─┘└┘
doc    └────┘                
txt    └────┘                
par    └────┘                
pid                         
st   ────────────────────────────┘└─
489  end
st   ──┘
490  
491  --AN INFINITE LEMMA THAT REQUIRES SOME MORE ST MACHINERY
492  lemma not_infinite_mul {x y : ℝ*} (hx : ¬ infinite x) (hy : ¬ infinite y) :
id                                 └┘         └──────┘          └──────┘ 
src                                └┘         └──────┘           └──────┘
typ                                └┘         └──────┘          └──────┘ 
doc                                └┘          └──────┘            └──────┘
493    ¬ infinite (x * y) :=
id      └──────┘    
src     └──────┘    
typ     └──────┘    
doc      └──────┘
494  have hx' : _ := exists_st_of_not_infinite hx, have hy' : _ := exists_st_of_not_infinite hy,
id                   └───────────────────────┘ └┘                  └───────────────────────┘ └┘
src                  └───────────────────────┘                     └───────────────────────┘
typ                  └───────────────────────┘ └┘                  └───────────────────────┘ └┘
495  Exists.cases_on hx' $ Exists.cases_on hy' $ λ r hr s hs, not_infinite_of_exists_st $
id   └─────────────┘ └─┘   └─────────────┘ └─┘      └┘  └┘  └───────────────────────┘
src  └─────────────┘       └─────────────┘                    └───────────────────────┘
typ  └─────────────┘ └─┘   └─────────────┘ └─┘      └┘  └┘  └───────────────────────┘
496  ⟨s * r, is_st_mul hs hr⟩
id        └───────┘ └┘ └┘
src         └───────┘
typ       └───────┘ └┘ └┘
497  ---
498  
499  lemma st_add {x y : ℝ*} (hx : ¬infinite x) (hy : ¬infinite y) : st (x + y) = st x + st y :=
id                       └┘        └──────┘         └──────┘     └┘       └┘   └┘ 
src                      └┘        └──────┘          └──────┘      └┘         └┘    └┘
typ                      └┘        └──────┘         └──────┘     └┘       └┘   └┘ 
doc                      └┘         └──────┘           └──────┘      └┘           └┘     └┘
500  have hx' : _ := is_st_st' hx,
id                   └───────┘ └┘
src                  └───────┘
typ                  └───────┘ └┘
501  have hy' : _ := is_st_st' hy,
id                   └───────┘ └┘
src                  └───────┘
typ                  └───────┘ └┘
502  have hxy : _ := is_st_st' (not_infinite_add hx hy),
id                   └───────┘  └──────────────┘ └┘ └┘
src                  └───────┘  └──────────────┘
typ                  └───────┘  └──────────────┘ └┘ └┘
503  have hxy' : _ := is_st_add hx' hy',
id                    └───────┘ └─┘ └─┘
src                   └───────┘
typ                   └───────┘ └─┘ └─┘
504  is_st_unique hxy hxy'
id   └──────────┘ └─┘ └──┘
src  └──────────┘
typ  └──────────┘ └─┘ └──┘
505  
506  lemma st_neg (x : ℝ*) : st (-x) = - st x :=
id                     └┘    └┘      └┘ 
src                    └┘    └┘       └┘
typ                    └┘    └┘      └┘ 
doc                    └┘    └┘          └┘
507  if h : infinite x
id   └┘     └──────┘ 
src  └┘     └──────┘
typ  └┘     └──────┘ 
doc         └──────┘
508  then by rw [st_infinite h, st_infinite (infinite_iff_infinite_neg.mp h), neg_zero]
id               └─────────┘   └─────────┘  └──────────────────────────┘    └──────┘
src          └──┘└─────────┘ └┘└─────────┘ └──────────────────────────┘ └─┘└──────┘└┘
typ          └──┘└─────────┘└┘└─────────┘ └──────────────────────────┘└─┘└──────┘└┘
doc          └──┘            └┘                                         └─┘        └┘
txt          └──┘            └┘                                         └─┘        └┘
par          └──┘            └┘                                         └─┘        └┘
pid            └┘            └┘                                         └─┘        
st          └────────────────┘└────────────────────────────────────────────┘└────────┘
509  else is_st_unique (is_st_st' (not_infinite_neg h)) (is_st_neg (is_st_st' h))
id        └──────────┘  └───────┘  └──────────────┘     └───────┘  └───────┘ 
src       └──────────┘  └───────┘  └──────────────┘      └───────┘  └───────┘
typ       └──────────┘  └───────┘  └──────────────┘     └───────┘  └───────┘ 
510  
511  lemma st_mul {x y : ℝ*} (hx : ¬infinite x) (hy : ¬infinite y) : st (x * y) = (st x) * (st y) :=
id                       └┘        └──────┘         └──────┘     └┘        └┘     └┘ 
src                      └┘        └──────┘          └──────┘      └┘          └┘      └┘
typ                      └┘        └──────┘         └──────┘     └┘        └┘     └┘ 
doc                      └┘         └──────┘           └──────┘      └┘            └┘       └┘
512  have hx' : _ := is_st_st' hx,
id                   └───────┘ └┘
src                  └───────┘
typ                  └───────┘ └┘
513  have hy' : _ := is_st_st' hy,
id                   └───────┘ └┘
src                  └───────┘
typ                  └───────┘ └┘
514  have hxy : _ := is_st_st' (not_infinite_mul hx hy),
id                   └───────┘  └──────────────┘ └┘ └┘
src                  └───────┘  └──────────────┘
typ                  └───────┘  └──────────────┘ └┘ └┘
515  have hxy' : _ := is_st_mul hx' hy',
id                    └───────┘ └─┘ └─┘
src                   └───────┘
typ                   └───────┘ └─┘ └─┘
516  is_st_unique hxy hxy'
id   └──────────┘ └─┘ └──┘
src  └──────────┘
typ  └──────────┘ └─┘ └──┘
517  
518  -- BASIC LEMMAS ABOUT INFINITESIMAL
519  
520  theorem infinitesimal_def {x : ℝ*} :
id                                  └┘
src                                 └┘
typ                                 └┘
doc                                 └┘
521    infinitesimal x ↔ (∀ r : ℝ, r > 0 → -(r : ℝ*) < x ∧ x < r) :=
id     └───────────┘                      └┘       
src    └───────────┘                         └┘        
typ    └───────────┘                      └┘       
doc    └───────────┘                             └┘
522  ⟨ λ hi r hr, by { convert (hi r hr), exact (zero_sub (of r)).symm, exact (zero_add (of r)).symm },
id       └┘  └┘                └┘  └┘          └──────┘  └┘                 └──────┘  └┘ 
src                    └──────┘        └────┘ └──────┘ └┘ └─────┘  └────┘ └──────┘ └┘ └──────┘
typ      └┘  └┘       └──────┘ └┘└┘  └────┘ └──────┘ └┘└─────┘  └────┘ └──────┘ └┘└──────┘
doc                    └──────┘        └────┘          └┘ └─────┘  └────┘          └┘ └──────┘
txt                    └──────┘        └────┘             └─────┘  └────┘             └──────┘
par                    └──────┘        └────┘             └─────┘  └────┘             └──────┘
pid                                                     └────┘                    └────┘└┘
st                  └──────────────────┘└────────────────────────────┘└─────────────────────────────┘└┘
523    λ hi d hd, by { convert (hi d hd), exact zero_sub (of d), exact zero_add (of d) } ⟩
id       └┘  └┘                └┘  └┘         └──────┘  └┘          └──────┘  └┘ 
src                    └──────┘        └────┘└──────┘ └┘   └────┘└──────┘ └┘ └┘
typ      └┘  └┘       └──────┘ └┘└┘  └────┘└──────┘ └┘  └────┘└──────┘ └┘└┘
doc                    └──────┘        └────┘         └┘   └────┘         └┘ └┘
txt                    └──────┘        └────┘              └────┘            └┘
par                    └──────┘        └────┘              └────┘            └┘
pid                                                                       
st                  └──────────────────┘└─────────────────────┘└──────────────────────┘└┘
524  
525  theorem lt_of_pos_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r > 0 → x < r :=
id                                           └┘    └───────────┘                    
src                                          └┘    └───────────┘                      
typ                                          └┘    └───────────┘                    
doc                                          └┘    └───────────┘
526  λ hi r hr, ((infinitesimal_def.mp hi) r hr).2
id     └┘  └┘    └───────────────┘└─┘ └┘   └┘ 
src               └───────────────┘└─┘          
typ    └┘  └┘    └───────────────┘└─┘ └┘   └┘ 
527  
528  theorem lt_neg_of_pos_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r > 0 → x > -r :=
id                                               └┘    └───────────┘                    
src                                              └┘    └───────────┘                       
typ                                              └┘    └───────────┘                    
doc                                              └┘    └───────────┘
529  λ hi r hr, ((infinitesimal_def.mp hi) r hr).1
id     └┘  └┘    └───────────────┘└─┘ └┘   └┘ 
src               └───────────────┘└─┘          
typ    └┘  └┘    └───────────────┘└─┘ └┘   └┘ 
530  
531  theorem gt_of_neg_of_infinitesimal {x : ℝ*} : infinitesimal x → ∀ r : ℝ, r < 0 → x > r :=
id                                           └┘    └───────────┘                    
src                                          └┘    └───────────┘                      
typ                                          └┘    └───────────┘                    
doc                                          └┘    └───────────┘
532  λ hi r hr, by convert ((infinitesimal_def.mp hi) (-r) (neg_pos.mpr hr)).1;
id     └┘  └┘               └──────────────────┘ └┘      └─────────┘ └┘
src                └──────┘  └──────────────────┘  └┘  └┘ └─────────┘  └──┘
typ    └┘  └┘     └──────┘  └──────────────────┘└┘└┘ └┘ └─────────┘└┘└──┘
doc                └──────┘                        └┘   └┘              └──┘
txt                └──────┘                        └┘   └┘              └──┘
par                └──────┘                        └┘   └┘              └──┘
pid                                               └┘   └┘              └┘└┘
st                └─────────────────────────────────────────────────────────────
533  exact (neg_neg (of r)).symm
id          └─────┘  └┘ 
src  └────┘ └─────┘ └┘ └───────
typ  └────┘ └─────┘ └┘└───────
doc  └────┘         └┘ └───────
txt  └────┘            └───────
par  └────┘            └───────
pid                   └────┘└─
st   ────────────────────────────
534  
src  
typ  
doc  
txt  
par  
pid  
st   
535  theorem abs_lt_real_iff_infinitesimal {x : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
536    infinitesimal x ↔ ∀ r : ℝ, r ≠ 0 → abs x < abs r :=
id     └───────────┘                 └─┘   └─┘ 
src    └───────────┘                   └─┘    └─┘
typ    └───────────┘                 └─┘   └─┘ 
doc    └───────────┘
537  ⟨ λ hi r hr, abs_lt.mpr (by rw [←of_eq_coe, ←of_abs U];
id       └┘  └┘  └────┘└──┘          └───────┘   └────┘ 
src               └────┘└──┘     └───┘└───────┘└─┘└────┘
typ      └┘  └┘  └────┘└──┘     └───┘└───────┘└─┘└────┘
doc                              └───┘         └─┘       
txt                              └───┘         └─┘       
par                              └───┘         └─┘       
pid                                └─┘         └─┘       
st                              └─────────────┘└─────────┘└─
538    exact infinitesimal_def.mp hi (abs r) (abs_pos_of_ne_zero hr)),
id           └──────────────────┘ └┘  └─┘    └────────────────┘ └┘
src    └────┘└──────────────────┘   └─┘ └┘ └────────────────┘  
typ    └────┘└──────────────────┘└┘ └─┘└┘ └────────────────┘└┘
doc    └────┘                           └┘                     
txt    └────┘                           └┘                     
par    └────┘                           └┘                     
pid                                    └┘                     
st   ──────────────────────────────────────────────────────────────┘
539    λ hR, infinitesimal_def.mpr $ λ r hr, abs_lt.mp $
id       └┘  └───────────────┘└──┘      └┘  └────┘└─┘
src          └───────────────┘└──┘           └────┘└─┘
typ      └┘  └───────────────┘└──┘      └┘  └────┘└─┘
540    (abs_of_pos $ of_lt_of_lt U hr : abs (r : ℝ*) = r) ▸ hR r $ ne_of_gt hr ⟩
id      └────────┘   └─────────┘  └┘   └─┘     └┘      └┘    └──────┘ └┘
src     └────────┘   └─────────┘       └─┘      └┘              └──────┘
typ     └────────┘   └─────────┘  └┘   └─┘     └┘      └┘    └──────┘ └┘
doc                                              └┘
541  
542  lemma infinitesimal_zero : infinitesimal 0 := is_st_refl_real 0
id                              └───────────┘      └─────────────┘
src                             └───────────┘      └─────────────┘
typ                             └───────────┘      └─────────────┘
doc                             └───────────┘
543  
544  lemma zero_of_infinitesimal_real {r : ℝ} : infinitesimal r → r = 0 := eq_of_is_st_real
id                                             └───────────┘           └──────────────┘
src                                            └───────────┘             └──────────────┘
typ                                            └───────────┘           └──────────────┘
doc                                             └───────────┘
545  
546  lemma zero_iff_infinitesimal_real {r : ℝ} : infinitesimal r ↔ r = 0 :=
id                                              └───────────┘    
src                                             └───────────┘      
typ                                             └───────────┘    
doc                                              └───────────┘
547  ⟨zero_of_infinitesimal_real, λ hr, by rw hr; exact infinitesimal_zero⟩
id    └────────────────────────┘    └┘        └┘        └────────────────┘
src   └────────────────────────┘           └─┘    └────┘└────────────────┘
typ   └────────────────────────┘    └┘     └─┘└┘  └────┘└────────────────┘
doc                                        └─┘    └────┘
txt                                        └─┘    └────┘
par                                        └─┘    └────┘
pid                                                   
st                                        └──────────────────────────────┘
548  
549  lemma infinitesimal_add {x y : ℝ*} :
id                                  └┘
src                                 └┘
typ                                 └┘
doc                                 └┘
550    infinitesimal x → infinitesimal y → infinitesimal (x + y) :=
id     └───────────┘    └───────────┘    └───────────┘    
src    └───────────┘     └───────────┘     └───────────┘    
typ    └───────────┘    └───────────┘    └───────────┘    
doc    └───────────┘     └───────────┘     └───────────┘
551  zero_add 0 ▸ is_st_add
id   └──────┘    └───────┘
src  └──────┘    └───────┘
typ  └──────┘    └───────┘
552  
553  lemma infinitesimal_neg {x : ℝ*} : infinitesimal x → infinitesimal (-x) :=
id                                └┘    └───────────┘    └───────────┘  
src                               └┘    └───────────┘     └───────────┘  
typ                               └┘    └───────────┘    └───────────┘  
doc                               └┘    └───────────┘     └───────────┘
554  (neg_zero : -(0 : ℝ) = 0) ▸ is_st_neg
id    └──────┘               └───────┘
src   └──────┘               └───────┘
typ   └──────┘               └───────┘
555  
556  lemma infinitesimal_neg_iff {x : ℝ*} : infinitesimal x ↔ infinitesimal (-x) :=
id                                    └┘    └───────────┘   └───────────┘  
src                                   └┘    └───────────┘    └───────────┘  
typ                                   └┘    └───────────┘   └───────────┘  
doc                                   └┘    └───────────┘     └───────────┘
557  ⟨infinitesimal_neg, λ h, (neg_neg x) ▸ @infinitesimal_neg (-x) h⟩
id    └───────────────┘       └─────┘     └───────────────┘    
src   └───────────────┘        └─────┘      └───────────────┘  
typ   └───────────────┘       └─────┘     └───────────────┘    
558  
559  lemma infinitesimal_mul {x y : ℝ*} :
id                                  └┘
src                                 └┘
typ                                 └┘
doc                                 └┘
560    infinitesimal x → infinitesimal y → infinitesimal (x * y) :=
id     └───────────┘    └───────────┘    └───────────┘    
src    └───────────┘     └───────────┘     └───────────┘    
typ    └───────────┘    └───────────┘    └───────────┘    
doc    └───────────┘     └───────────┘     └───────────┘
561  zero_mul 0 ▸ is_st_mul
id   └──────┘    └───────┘
src  └──────┘    └───────┘
typ  └──────┘    └───────┘
562  
563  theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} :
id                                                 
src                                                
typ                                                
564    tendsto f at_top (𝓝 0) → infinitesimal (of_seq f) :=
id     └─────┘  └────┘        └───────────┘  └────┘ 
src    └─────┘   └────┘        └───────────┘  └────┘
typ    └─────┘  └────┘        └───────────┘  └────┘ 
doc    └─────┘   └────┘        └───────────┘
565  λ hf d hd, by rw [←of_eq_coe, ←of_eq_coe, sub_eq_add_neg,
id     └┘  └┘          └───────┘   └───────┘  └────────────┘
src                └───┘└───────┘└─┘└───────┘└┘└────────────┘└─
typ    └┘  └┘     └───┘└───────┘└─┘└───────┘└┘└────────────┘└─
doc                └───┘         └─┘         └┘              └─
txt                └───┘         └─┘         └┘              └─
par                └───┘         └─┘         └┘              └─
pid                  └─┘         └─┘         └┘              └─
st                └─────────────┘└──────────┘└──────────────┘└─
566    ←of_neg, ←of_add, ←of_add, zero_add, zero_add, of_eq_coe, of_eq_coe];
id      └────┘   └────┘   └────┘  └──────┘  └──────┘  └───────┘  └───────┘
src  ──┘└────┘└─┘└────┘└─┘└────┘└┘└──────┘└┘└──────┘└┘└───────┘└┘└───────┘
typ  ──┘└────┘└─┘└────┘└─┘└────┘└┘└──────┘└┘└──────┘└┘└───────┘└┘└───────┘
doc  ──┘      └─┘      └─┘      └┘        └┘        └┘         └┘         
txt  ──┘      └─┘      └─┘      └┘        └┘        └┘         └┘         
par  ──┘      └─┘      └─┘      └┘        └┘        └┘         └┘         
pid  ──┘      └─┘      └─┘      └┘        └┘        └┘         └┘         
st   ────────┘└───────┘└───────┘└────────┘└────────┘└─────────┘└─────────┘└─
567  exact ⟨neg_lt_of_tendsto_zero_of_pos hf hd, lt_of_tendsto_zero_of_pos hf hd⟩
id          └───────────────────────────┘        └───────────────────────┘ └┘ └┘
src  └────┘ └───────────────────────────┘    └┘└───────────────────────┘    └─
typ  └────┘ └───────────────────────────┘    └┘└───────────────────────┘└┘└┘└─
doc  └────┘                                  └┘                             └─
txt  └────┘                                  └┘                             └─
par  └────┘                                  └┘                             └─
pid                                         └┘                             
st   ─────────────────────────────────────────────────────────────────────────────
568  
src  
typ  
doc  
txt  
par  
pid  
st   
569  theorem infinitesimal_epsilon : infinitesimal ε :=
id                                   └───────────┘ 
src                                  └───────────┘ 
typ                                  └───────────┘ 
doc                                  └───────────┘ 
570  infinitesimal_of_tendsto_zero tendsto_inverse_at_top_nhds_0_nat
id   └───────────────────────────┘ └───────────────────────────────┘
src  └───────────────────────────┘ └───────────────────────────────┘
typ  └───────────────────────────┘ └───────────────────────────────┘
571  
572  lemma not_real_of_infinitesimal_ne_zero (x : ℝ*) :
id                                                └┘
src                                               └┘
typ                                               └┘
doc                                               └┘
573    infinitesimal x → x ≠ 0 → ∀ r : ℝ, x ≠ of r :=
id     └───────────┘                    └┘ 
src    └───────────┘                       └┘
typ    └───────────┘                    └┘ 
doc    └───────────┘                          └┘
574  λ hi hx r hr, hx (is_st_unique (hr.symm ▸ is_st_refl_real r : is_st x r) hi ▸ hr : x = of 0)
id     └┘ └┘  └┘  └┘  └──────────┘  └┘└───┘  └─────────────┘    └───┘    └┘  └┘     └┘
src                    └──────────┘    └───┘  └─────────────┘     └───┘                  └┘
typ    └┘ └┘  └┘  └┘  └──────────┘  └┘└───┘  └─────────────┘    └───┘    └┘  └┘     └┘
doc                                                                └───┘                    └┘
575  
576  theorem infinitesimal_sub_is_st {x : ℝ*} {r : ℝ} (hxr : is_st x r) : infinitesimal (x - r) :=
id                                        └┘                └───┘      └───────────┘    
src                                       └┘                └───┘        └───────────┘    
typ                                       └┘                └───┘      └───────────┘    
doc                                       └┘                 └───┘        └───────────┘
577  show is_st (x + -r) 0, by rw ←add_neg_self r; exact is_st_add hxr (is_st_refl_real (-r))
id        └───┘                └──────────┘         └───────┘ └─┘  └─────────────┘  
src       └───┘              └──┘└──────────┘   └────┘└───────┘    └─────────────┘  └──
typ       └───┘            └──┘└──────────┘  └────┘└───────┘└─┘ └─────────────┘ └──
doc       └───┘                └──┘               └────┘                               └──
txt                            └──┘               └────┘                               └──
par                            └──┘               └────┘                               └──
pid                              └┘                                                   └┘
st                            └───────────────────────────────────────────────────────────────
578  
src  
typ  
doc  
txt  
par  
pid  
st   
579  theorem infinitesimal_sub_st {x : ℝ*} (hx : ¬infinite x) : infinitesimal (x - st x) :=
id                                     └┘        └──────┘     └───────────┘    └┘ 
src                                    └┘        └──────┘      └───────────┘     └┘
typ                                    └┘        └──────┘     └───────────┘    └┘ 
doc                                    └┘         └──────┘      └───────────┘      └┘
580  infinitesimal_sub_is_st $ is_st_st' hx
id   └─────────────────────┘   └───────┘ └┘
src  └─────────────────────┘   └───────┘
typ  └─────────────────────┘   └───────┘ └┘
581  
582  lemma infinite_pos_iff_infinitesimal_inv_pos {x : ℝ*} :
id                                                     └┘
src                                                    └┘
typ                                                    └┘
doc                                                    └┘
583    infinite_pos x ↔ (infinitesimal x⁻¹ ∧ x⁻¹ > 0) :=
id     └──────────┘    └───────────┘ └┘  └┘ 
src    └──────────┘     └───────────┘  └┘   └┘ 
typ    └──────────┘    └───────────┘ └┘  └┘ 
doc    └──────────┘      └───────────┘
584  ⟨ λ hip, ⟨ infinitesimal_def.mpr $ λ r hr,
id       └─┘    └───────────────┘└──┘      └┘
src             └───────────────┘└──┘
typ      └─┘    └───────────────┘└──┘      └┘
585    ⟨ lt_trans (of_lt_of_lt U (neg_neg_of_pos hr)) (inv_pos (hip 0)),
id       └──────┘  └─────────┘   └────────────┘ └┘    └─────┘  └─┘
src      └──────┘  └─────────┘   └────────────┘       └─────┘
typ      └──────┘  └─────────┘   └────────────┘ └┘    └─────┘  └─┘
586      (inv_lt (of_lt_of_lt U hr) (hip 0)).mp (by convert hip r⁻¹) ⟩,
id        └────┘  └─────────┘  └┘   └─┘    └┘              └─┘ └┘
src       └────┘  └─────────┘              └┘      └──────┘    └┘
typ       └────┘  └─────────┘  └┘   └─┘    └┘      └──────┘└─┘└┘
doc                                                 └──────┘   
txt                                                 └──────┘   
par                                                 └──────┘   
pid                                                           
st                                                 └──────────────┘
587    inv_pos $ hip 0 ⟩,
id     └─────┘   └─┘
src    └─────┘
typ    └─────┘   └─┘
588    λ ⟨hi, hp⟩ r, @classical.by_cases (r = 0) (x > (r : ℝ*)) (λ h, eq.substr h (inv_pos'.mp hp)) $
id       └┘  └┘     └────────────────┘              └┘        └───────┘   └──────┘└─┘
src                   └────────────────┘                 └┘         └───────┘    └──────┘└─┘
typ      └┘  └┘     └────────────────┘              └┘        └───────┘   └──────┘└─┘
doc                                                        └┘
589    λ h, lt_of_le_of_lt (of_le_of_le (le_abs_self r))
id         └────────────┘  └─────────┘  └─────────┘ 
src         └────────────┘  └─────────┘  └─────────┘
typ        └────────────┘  └─────────┘  └─────────┘ 
st                                     
590    ((inv_lt_inv (inv_pos'.mp hp) (of_lt_of_lt U (abs_pos_of_ne_zero h))).mp
id       └────────┘  └──────┘└─┘      └─────────┘   └────────────────┘    └┘
src      └────────┘  └──────┘└─┘      └─────────┘   └────────────────┘     └┘
typ      └────────┘  └──────┘└─┘      └─────────┘   └────────────────┘    └┘
591    ((infinitesimal_def.mp hi) ((abs r)⁻¹) (inv_pos (abs_pos_of_ne_zero h))).2) ⟩
id       └───────────────┘└─┘       └─┘  └┘   └─────┘  └────────────────┘    
src      └───────────────┘└─┘       └─┘   └┘   └─────┘  └────────────────┘     
typ      └───────────────┘└─┘       └─┘  └┘   └─────┘  └────────────────┘    
592  
593  lemma infinite_neg_iff_infinitesimal_inv_neg {x : ℝ*} :
id                                                     └┘
src                                                    └┘
typ                                                    └┘
doc                                                    └┘
594    infinite_neg x ↔ (infinitesimal x⁻¹ ∧ x⁻¹ < 0) :=
id     └──────────┘    └───────────┘ └┘  └┘ 
src    └──────────┘     └───────────┘  └┘   └┘ 
typ    └──────────┘    └───────────┘ └┘  └┘ 
doc    └──────────┘      └───────────┘
595  ⟨ λ hin, have hin' : _ := infinite_pos_iff_infinitesimal_inv_pos.mp
id       └─┘                   └────────────────────────────────────┘└─┘
src                            └────────────────────────────────────┘└─┘
typ      └─┘                   └────────────────────────────────────┘└─┘
596    (infinite_pos_neg_of_infinite_neg hin),
id      └──────────────────────────────┘ └─┘
src     └──────────────────────────────┘
typ     └──────────────────────────────┘ └─┘
597    by rwa [infinitesimal_neg_iff, ←neg_pos,
id             └───────────────────┘   └─────┘
src       └───┘└───────────────────┘└─┘└─────┘└─
typ       └───┘└───────────────────┘└─┘└─────┘└─
doc       └───┘                     └─┘       └─
txt       └───┘                     └─┘       └─
par       └───┘                     └─┘       └─
pid          └┘                     └─┘       └─
st       └─────────────────────────┘└────────┘└─
598      neg_inv (λ h0, lt_irrefl x (by convert hin 0) : x ≠ 0)],
id       └─────┘        └───────┘              └─┘        
src  ───┘└─────┘  └───┘└───────┘    └──────┘   └┘└──┘ └──┘
typ  ───┘└─────┘  └───┘└───────┘   └──────┘└─┘└┘└──┘ └──┘
doc  ───┘         └───┘             └──────┘   └┘└──┘  └──┘
txt  ───┘         └───┘             └──────┘   └┘└──┘  └──┘
par  ───┘         └───┘             └──────┘   └┘└──┘  └──┘
pid  ───┘         └───┘             └───────┘   └────┘  └──┘
st   ─────────────────────────────────┘└────────────┘└────────┘
599    λ hin, have h0 : x ≠ 0 := λ h0, (lt_irrefl (0 : ℝ*) (by convert hin.2; rw [h0, inv_zero])),
id       └─┘                     └┘   └───────┘      └┘              └─┘        └┘  └──────┘
src                                    └───────┘      └┘      └──────┘   └┘  └──┘  └┘└──────┘
typ      └─┘                     └┘   └───────┘      └┘      └──────┘└─┘└┘  └──┘└┘└┘└──────┘
doc                                                    └┘      └──────┘   └┘  └──┘  └┘        
txt                                                            └──────┘   └┘  └──┘  └┘        
par                                                            └──────┘   └┘  └──┘  └┘        
pid                                                                      └┘    └┘  └┘        
st                                                            └──────────────────┘└┘└────────┘
600    by rwa [←neg_pos, infinitesimal_neg_iff, neg_inv h0,
id              └─────┘  └───────────────────┘  └─────┘ └┘
src       └────┘└─────┘└┘└───────────────────┘└┘└─────┘  └─
typ       └────┘└─────┘└┘└───────────────────┘└┘└─────┘└┘└─
doc       └────┘       └┘                     └┘         └─
txt       └────┘       └┘                     └┘         └─
par       └────┘       └┘                     └┘         └─
pid          └─┘       └┘                     └┘         └─
st       └────────────┘└─────────────────────┘└──────────┘└─
601      ←infinite_pos_iff_infinitesimal_inv_pos, ←infinite_neg_iff_infinite_pos_neg] at hin ⟩
id        └────────────────────────────────────┘   └───────────────────────────────┘
src  ────┘└────────────────────────────────────┘└─┘└───────────────────────────────┘└───────┘
typ  ────┘└────────────────────────────────────┘└─┘└───────────────────────────────┘└───────┘
doc  ────┘                                      └─┘                                 └───────┘
txt  ────┘                                      └─┘                                 └───────┘
par  ────┘                                      └─┘                                 └───────┘
pid  ────┘                                      └─┘                                 └─────┘
st   ──────────────────────────────────────────┘└──────────────────────────────────┘└──────┘
602  
603  theorem infinitesimal_inv_of_infinite {x : ℝ*} : infinite x → infinitesimal x⁻¹ :=
id                                              └┘    └──────┘    └───────────┘ └┘
src                                             └┘    └──────┘     └───────────┘  └┘
typ                                             └┘    └──────┘    └───────────┘ └┘
doc                                             └┘    └──────┘     └───────────┘
604  λ hi, or.cases_on hi
id     └┘  └─────────┘ └┘
src        └─────────┘
typ    └┘  └─────────┘ └┘
605   (λ hip, (infinite_pos_iff_infinitesimal_inv_pos.mp hip).1)
id       └─┘   └────────────────────────────────────┘└─┘ └─┘ 
src            └────────────────────────────────────┘└─┘     
typ      └─┘   └────────────────────────────────────┘└─┘ └─┘ 
606   (λ hin, (infinite_neg_iff_infinitesimal_inv_neg.mp hin).1)
id       └─┘   └────────────────────────────────────┘└─┘ └─┘ 
src            └────────────────────────────────────┘└─┘     
typ      └─┘   └────────────────────────────────────┘└─┘ └─┘ 
607  
608  theorem infinite_of_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) (hi : infinitesimal x⁻¹ ) :
id                                              └┘                   └───────────┘ └┘
src                                             └┘                    └───────────┘  └┘
typ                                             └┘                   └───────────┘ └┘
doc                                             └┘                     └───────────┘
609    infinite x :=
id     └──────┘ 
src    └──────┘
typ    └──────┘ 
doc    └──────┘
610  begin
st   └─────
611    cases (lt_or_gt_of_ne h0) with hn hp,
id            └────────────┘ └┘
src    └────┘ └────────────┘  └──────────┘
typ    └────┘ └────────────┘└┘└──────────┘
doc    └────┘                 └──────────┘
txt    └────┘                 └──────────┘
par    └────┘                 └──────────┘
pid                          └─────────┘
st   ─────────────────────────────────────┘└─
612    { exact or.inr (infinite_neg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_neg'.mpr hn⟩) },
id             └────┘  └────────────────────────────────────────┘  └┘  └──────────┘ └┘
src      └────┘└────┘ └────────────────────────────────────────┘   └┘└──────────┘  └─┘
typ      └────┘└────┘ └────────────────────────────────────────┘ └┘└┘└──────────┘└┘└─┘
doc      └────┘                                                    └┘              └─┘
txt      └────┘                                                    └┘              └─┘
par      └────┘                                                    └┘              └─┘
pid                                                               └┘              └┘
st   ───┘└──────────────────────────────────────────────────────────────────────────────┘└┘
613    { exact or.inl (infinite_pos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos'.mpr hp⟩) }
id             └────┘  └────────────────────────────────────────┘  └┘  └──────────┘ └┘
src      └────┘└────┘ └────────────────────────────────────────┘   └┘└──────────┘  └─┘
typ      └────┘└────┘ └────────────────────────────────────────┘ └┘└┘└──────────┘└┘└─┘
doc      └────┘                                                    └┘              └─┘
txt      └────┘                                                    └┘              └─┘
par      └────┘                                                    └┘              └─┘
pid                                                               └┘              └┘
st   ───────────────────────────────────────────────────────────────────────────────────┘└─
614  end
st   ──┘
615  
616  theorem infinite_iff_infinitesimal_inv {x : ℝ*} (h0 : x ≠ 0) : infinite x ↔ infinitesimal x⁻¹ :=
id                                               └┘               └──────┘   └───────────┘ └┘
src                                              └┘                └──────┘    └───────────┘  └┘
typ                                              └┘               └──────┘   └───────────┘ └┘
doc                                              └┘                 └──────┘     └───────────┘
617  ⟨ infinitesimal_inv_of_infinite, infinite_of_infinitesimal_inv h0 ⟩
id     └───────────────────────────┘  └───────────────────────────┘ └┘
src    └───────────────────────────┘  └───────────────────────────┘
typ    └───────────────────────────┘  └───────────────────────────┘ └┘
618  
619  lemma infinitesimal_pos_iff_infinite_pos_inv {x : ℝ*} :
id                                                     └┘
src                                                    └┘
typ                                                    └┘
doc                                                    └┘
620    infinite_pos x⁻¹ ↔ (infinitesimal x ∧ x > 0) :=
id     └──────────┘ └┘   └───────────┘    
src    └──────────┘  └┘   └───────────┘      
typ    └──────────┘ └┘   └───────────┘    
doc    └──────────┘        └───────────┘
621  by convert infinite_pos_iff_infinitesimal_inv_pos; simp only [inv_inv']
id              └────────────────────────────────────┘             └──────┘
src     └──────┘└────────────────────────────────────┘  └─────────┘└──────┘└─
typ     └──────┘└────────────────────────────────────┘  └─────────┘└──────┘└─
doc     └──────┘                                        └─────────┘        └─
txt     └──────┘                                        └─────────┘        └─
par     └──────┘                                        └─────────┘        └─
pid                                                        └──┘└┘        
st     └─────────────────────────────────────────────────────────────────────
622  
src  
typ  
doc  
txt  
par  
pid  
st   
623  lemma infinitesimal_neg_iff_infinite_neg_inv {x : ℝ*} :
id                                                     └┘
src                                                    └┘
typ                                                    └┘
doc                                                    └┘
624    infinite_neg x⁻¹ ↔ (infinitesimal x ∧ x < 0) :=
id     └──────────┘ └┘   └───────────┘    
src    └──────────┘  └┘   └───────────┘      
typ    └──────────┘ └┘   └───────────┘    
doc    └──────────┘        └───────────┘
625  by convert infinite_neg_iff_infinitesimal_inv_neg; simp only [inv_inv']
id              └────────────────────────────────────┘             └──────┘
src     └──────┘└────────────────────────────────────┘  └─────────┘└──────┘└─
typ     └──────┘└────────────────────────────────────┘  └─────────┘└──────┘└─
doc     └──────┘                                        └─────────┘        └─
txt     └──────┘                                        └─────────┘        └─
par     └──────┘                                        └─────────┘        └─
pid                                                        └──┘└┘        
st     └─────────────────────────────────────────────────────────────────────
626  
src  
typ  
doc  
txt  
par  
pid  
st   
627  theorem infinitesimal_iff_infinite_inv {x : ℝ*} (h : x ≠ 0) : infinitesimal x ↔ infinite x⁻¹ :=
id                                               └┘              └───────────┘   └──────┘ └┘
src                                              └┘               └───────────┘    └──────┘  └┘
typ                                              └┘              └───────────┘   └──────┘ └┘
doc                                              └┘                └───────────┘     └──────┘
628  by convert (infinite_iff_infinitesimal_inv (inv_ne_zero h)).symm; simp only [inv_inv']
id               └────────────────────────────┘  └─────────┘                     └──────┘
src     └──────┘ └────────────────────────────┘ └─────────┘ └─────┘  └─────────┘└──────┘└─
typ     └──────┘ └────────────────────────────┘ └─────────┘└─────┘  └─────────┘└──────┘└─
doc     └──────┘                                            └─────┘  └─────────┘        └─
txt     └──────┘                                            └─────┘  └─────────┘        └─
par     └──────┘                                            └─────┘  └─────────┘        └─
pid                                                        └────┘      └──┘└┘        
st     └────────────────────────────────────────────────────────────────────────────────────
629  
src  
typ  
doc  
txt  
par  
pid  
st   
630  -- ST STUFF THAT REQUIRES INFINITESIMAL MACHINERY
src  ──────────────────────────────────────────────────
typ  ──────────────────────────────────────────────────
doc  ──────────────────────────────────────────────────
txt  ──────────────────────────────────────────────────
par  ──────────────────────────────────────────────────
pid  ──────────────────────────────────────────────────
st   ──────────────────────────────────────────────────
631  
src  
typ  
doc  
txt  
par  
pid  
st   
632  theorem is_st_of_tendsto {f : ℕ → ℝ} {r : ℝ} (hf : tendsto f at_top (𝓝 r)) :
id                                                   └─────┘  └────┘   
src                                                  └─────┘   └────┘  
typ                                                  └─────┘  └────┘   
doc                                                     └─────┘   └────┘  
633    is_st (of_seq f) r :=
id     └───┘  └────┘   
src    └───┘  └────┘
typ    └───┘  └────┘   
doc    └───┘
634  have hg : tendsto (λ n, f n - r) at_top (𝓝 0) :=
id             └─────┘           └────┘  
src            └─────┘               └────┘  
typ            └─────┘           └────┘  
doc            └─────┘                └────┘  
635    (sub_self r) ▸ (hf.sub tendsto_const_nhds),
id      └──────┘     └┘└──┘ └────────────────┘
src     └──────┘        └──┘ └────────────────┘
typ     └──────┘     └┘└──┘ └────────────────┘
636  by rw [←(zero_add r), ←(sub_add_cancel f (λ n, r))];
id            └──────┘      └────────────┘        
src     └───┘ └──────┘ └──┘ └────────────┘   └──┘ └─┘
typ     └───┘ └──────┘└──┘ └────────────┘  └──┘└─┘
doc     └───┘          └──┘                  └──┘ └─┘
txt     └───┘          └──┘                  └──┘ └─┘
par     └───┘          └──┘                  └──┘ └─┘
pid       └─┘          └──┘                  └──┘ └─┘
st     └────────────────┘└────────────────────────────┘└─
637  exact is_st_add (infinitesimal_of_tendsto_zero hg) (is_st_refl_real r)
id         └───────┘  └───────────────────────────┘ └┘   └─────────────┘ 
src  └────┘└───────┘ └───────────────────────────┘  └┘ └─────────────┘ └─
typ  └────┘└───────┘ └───────────────────────────┘└┘└┘ └─────────────┘└─
doc  └────┘                                         └┘                 └─
txt  └────┘                                         └┘                 └─
par  └────┘                                         └┘                 └─
pid                                                └┘                 
st   ───────────────────────────────────────────────────────────────────────
638  
src  
typ  
doc  
txt  
par  
pid  
st   
639  lemma is_st_inv {x : ℝ*} {r : ℝ} (hi : ¬ infinitesimal x) : is_st x r → is_st x⁻¹ r⁻¹ :=
id                        └┘                └───────────┘     └───┘     └───┘ └┘ └┘
src                       └┘                └───────────┘      └───┘       └───┘  └┘  └┘
typ                       └┘                └───────────┘     └───┘     └───┘ └┘ └┘
doc                       └┘                  └───────────┘      └───┘       └───┘
640  λ hxr, have h : x ≠ 0 := (λ h, hi (h.symm ▸ infinitesimal_zero)),
id     └─┘                       └┘  └───┘  └────────────────┘
src                                     └───┘  └────────────────┘
typ    └─┘                       └┘  └───┘  └────────────────┘
641  have H : _ := exists_st_of_not_infinite $ not_imp_not.mpr (infinitesimal_iff_infinite_inv h).mpr hi,
id                 └───────────────────────┘   └─────────┘└──┘  └────────────────────────────┘  └─┘  └┘
src                └───────────────────────┘   └─────────┘└──┘  └────────────────────────────┘   └─┘
typ                └───────────────────────┘   └─────────┘└──┘  └────────────────────────────┘  └─┘  └┘
642  Exists.cases_on H $ λ s hs,
id   └─────────────┘       └┘
src  └─────────────┘
typ  └─────────────┘       └┘
643  have H' : is_st 1 (r * s) := mul_inv_cancel h ▸ is_st_mul hxr hs,
id             └───┘           └────────────┘   └───────┘ └─┘ └┘
src            └───┘             └────────────┘    └───────┘
typ            └───┘           └────────────┘   └───────┘ └─┘ └┘
doc            └───┘
644  have H'' : s = r⁻¹ := one_div_eq_inv r ▸ eq_one_div_of_mul_eq_one (eq_of_is_st_real H').symm,
id                └┘    └────────────┘   └──────────────────────┘  └──────────────┘ └┘ └──┘
src                 └┘    └────────────┘    └──────────────────────┘  └──────────────┘    └──┘
typ               └┘    └────────────┘   └──────────────────────┘  └──────────────┘ └┘ └──┘
645  H'' ▸ hs
id   └─┘  └┘
src      
typ  └─┘  └┘
646  
647  lemma st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹ :=
id                     └┘    └┘ └┘   └┘  └┘
src                    └┘    └┘  └┘   └┘   └┘
typ                    └┘    └┘ └┘   └┘  └┘
doc                    └┘    └┘        └┘
648  begin
st   └─────
649    by_cases h0 : x = 0,
id                    
src    └───────┘  └─┘ └┘
typ    └───────┘  └─┘└┘
doc    └───────┘  └─┘  └┘
txt    └───────┘  └─┘  └┘
par    └───────┘  └─┘  └┘
pid              └─┘  
st   ────────────────────┘└─
650    rw [h0, inv_zero, ←of_zero, of_eq_coe, st_id_real, inv_zero],
id         └┘  └──────┘   └─────┘  └───────┘  └────────┘  └──────┘
src    └──┘  └┘└──────┘└─┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘
typ    └──┘└┘└┘└──────┘└─┘└─────┘└┘└───────┘└┘└────────┘└┘└──────┘
doc    └──┘  └┘        └─┘       └┘         └┘          └┘        
txt    └──┘  └┘        └─┘       └┘         └┘          └┘        
par    └──┘  └┘        └─┘       └┘         └┘          └┘        
pid      └┘  └┘        └─┘       └┘         └┘          └┘        
st   ───────┘└────────┘└────────┘└─────────┘└──────────┘└────────┘└──
651    by_cases h1 : infinitesimal x,
id                   └───────────┘ 
src    └───────┘  └─┘└───────────┘
typ    └───────┘  └─┘└───────────┘
doc    └───────┘  └─┘└───────────┘
txt    └───────┘  └─┘             
par    └───────┘  └─┘             
pid              └─┘             
st   ──────────────────────────────┘└─
652    rw [st_infinite ((infinitesimal_iff_infinite_inv h0).mp h1), st_of_is_st h1, inv_zero],
id         └─────────┘   └────────────────────────────┘ └┘     └┘   └─────────┘ └┘  └──────┘
src    └──┘└─────────┘  └────────────────────────────┘  └───┘  └─┘└─────────┘  └┘└──────┘
typ    └──┘└─────────┘  └────────────────────────────┘└┘└───┘└┘└─┘└─────────┘└┘└┘└──────┘
doc    └──┘                                             └───┘  └─┘             └┘        
txt    └──┘                                             └───┘  └─┘             └┘        
par    └──┘                                             └───┘  └─┘             └┘        
pid      └┘                                             └───┘  └─┘             └┘        
st   ────────────────────────────────────────────────────────────┘└──────────────┘└────────┘└──
653    by_cases h2 : infinite x,
id                   └──────┘ 
src    └───────┘  └─┘└──────┘
typ    └───────┘  └─┘└──────┘
doc    └───────┘  └─┘└──────┘
txt    └───────┘  └─┘        
par    └───────┘  └─┘        
pid              └─┘        
st   ─────────────────────────┘└─
654    rw [st_of_is_st (infinitesimal_inv_of_infinite h2), st_infinite h2, inv_zero],
id         └─────────┘  └───────────────────────────┘ └┘   └─────────┘ └┘  └──────┘
src    └──┘└─────────┘ └───────────────────────────┘  └─┘└─────────┘  └┘└──────┘
typ    └──┘└─────────┘ └───────────────────────────┘└┘└─┘└─────────┘└┘└┘└──────┘
doc    └──┘                                           └─┘             └┘        
txt    └──┘                                           └─┘             └┘        
par    └──┘                                           └─┘             └┘        
pid      └┘                                           └─┘             └┘        
st   ───────────────────────────────────────────────────┘└──────────────┘└────────┘└──
655    exact st_of_is_st (is_st_inv h1 (is_st_st' h2)),
id           └─────────┘  └───────┘ └┘  └───────┘ └┘
src    └────┘└─────────┘ └───────┘   └───────┘  └┘
typ    └────┘└─────────┘ └───────┘└┘ └───────┘└┘└┘
doc    └────┘                                   └┘
txt    └────┘                                   └┘
par    └────┘                                   └┘
pid                                            └┘
st   ────────────────────────────────────────────────┘└─
656  end
st   ──┘
657  
658  -- INFINITE STUFF THAT REQUIRES INFINITESIMAL MACHINERY
659  
660  lemma infinite_pos_omega : infinite_pos ω :=
id                              └──────────┘ 
src                             └──────────┘ 
typ                             └──────────┘ 
doc                             └──────────┘ 
661  infinite_pos_iff_infinitesimal_inv_pos.mpr ⟨infinitesimal_epsilon, epsilon_pos⟩
id   └────────────────────────────────────┘└──┘  └───────────────────┘  └─────────┘
src  └────────────────────────────────────┘└──┘  └───────────────────┘  └─────────┘
typ  └────────────────────────────────────┘└──┘  └───────────────────┘  └─────────┘
662  
663  lemma infinite_omega : infinite ω :=
id                          └──────┘ 
src                         └──────┘ 
typ                         └──────┘ 
doc                         └──────┘ 
664  (infinite_iff_infinitesimal_inv omega_ne_zero).mpr infinitesimal_epsilon
id    └────────────────────────────┘ └───────────┘ └─┘  └───────────────────┘
src   └────────────────────────────┘ └───────────┘ └─┘  └───────────────────┘
typ   └────────────────────────────┘ └───────────┘ └─┘  └───────────────────┘
665  
666  lemma infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
667    infinite_pos x → ¬ infinitesimal y → y > 0 → infinite_pos (x * y) :=
id     └──────────┘     └───────────┘          └──────────┘    
src    └──────────┘      └───────────┘            └──────────┘    
typ    └──────────┘     └───────────┘          └──────────┘    
doc    └──────────┘       └───────────┘             └──────────┘
668  λ hx hy₁ hy₂ r, have hy₁' : _ := not_forall.mp (by rw infinitesimal_def at hy₁; exact hy₁),
id     └┘ └─┘ └─┘                    └────────┘└─┘        └───────────────┘               └─┘
src                                   └────────┘└─┘     └─┘└───────────────┘└─────┘  └────┘
typ    └┘ └─┘ └─┘                    └────────┘└─┘     └─┘└───────────────┘└─────┘  └────┘└─┘
doc                                                     └─┘                 └─────┘  └────┘
txt                                                     └─┘                 └─────┘  └────┘
par                                                     └─┘                 └─────┘  └────┘
pid                                                                        └─────┘       
st                                                     └─────────────────────────────────────┘
669  Exists.dcases_on hy₁' $ λ r₁ hy₁'',
id   └──────────────┘ └──┘     └┘ └───┘
src  └──────────────┘
typ  └──────────────┘ └──┘     └┘ └───┘
670  have hyr : _ := by rw [not_imp, ←abs_lt, not_lt, abs_of_pos hy₂] at hy₁''; exact hy₁'',
id                          └─────┘   └────┘  └────┘  └────────┘ └─┘                  └───┘
src                     └──┘└─────┘└─┘└────┘└┘└────┘└┘└────────┘   └────────┘  └────┘
typ                     └──┘└─────┘└─┘└────┘└┘└────┘└┘└────────┘└─┘└────────┘  └────┘└───┘
doc                     └──┘       └─┘      └┘      └┘             └────────┘  └────┘
txt                     └──┘       └─┘      └┘      └┘             └────────┘  └────┘
par                     └──┘       └─┘      └┘      └┘             └────────┘  └────┘
pid                       └┘       └─┘      └┘      └┘             └───────┘       
st                     └──────────┘└───────┘└──────┘└──────────────┘└────────────────────┘
671  by rw [←div_mul_cancel r (ne_of_gt hyr.1), ←of_eq_coe, of_mul];
id           └────────────┘   └──────┘ └─┘      └───────┘  └────┘
src     └───┘└────────────┘  └──────┘   └────┘└───────┘└┘└────┘
typ     └───┘└────────────┘ └──────┘└─┘└────┘└───────┘└┘└────┘
doc     └───┘                           └────┘         └┘      
txt     └───┘                           └────┘         └┘      
par     └───┘                           └────┘         └┘      
pid       └─┘                           └────┘         └┘      
st     └─────────────────────────────────────┘└──────────┘└──────┘└─
672  exact mul_lt_mul (hx (r / r₁)) hyr.2 (of_lt_of_lt U hyr.1) (le_of_lt (hx 0))
id         └────────┘        └┘          └─────────┘  └─┘     └──────┘  └┘
src  └────┘└────────┘       └─┘   └─┘ └─────────┘   └──┘ └──────┘   └────
typ  └────┘└────────┘    └┘└─┘   └─┘ └─────────┘└─┘└──┘ └──────┘ └┘└────
doc  └────┘                  └─┘   └─┘                └──┘            └────
txt  └────┘                  └─┘   └─┘                └──┘            └────
par  └────┘                  └─┘   └─┘                └──┘            └────
pid                         └─┘   └─┘                └──┘            └──┘
st   ─────────────────────────────────────────────────────────────────────────────
673  
src  
typ  
doc  
txt  
par  
pid  
st   
674  lemma infinite_pos_mul_of_not_infinitesimal_pos_infinite_pos {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
675    ¬ infinitesimal x → 0 < x → infinite_pos y → infinite_pos (x * y) :=
id      └───────────┘          └──────────┘    └──────────┘    
src     └───────────┘            └──────────┘     └──────────┘    
typ     └───────────┘          └──────────┘    └──────────┘    
doc      └───────────┘             └──────────┘     └──────────┘
676  λ hx hp hy, by rw mul_comm; exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos hy hx hp
id     └┘ └┘ └┘        └──────┘        └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                 └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘      
typ    └┘ └┘ └┘     └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘└┘└┘└┘
doc                 └─┘          └────┘                                                            
txt                 └─┘          └────┘                                                            
par                 └─┘          └────┘                                                            
pid                                                                                              
st                 └───────────────────────────────────────────────────────────────────────────────────
677  
src  
typ  
doc  
txt  
par  
pid  
st   
678  lemma infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
679    infinite_neg x → ¬ infinitesimal y → y < 0 → infinite_pos (x * y) :=
id     └──────────┘     └───────────┘          └──────────┘    
src    └──────────┘      └───────────┘            └──────────┘    
typ    └──────────┘     └───────────┘          └──────────┘    
doc    └──────────┘       └───────────┘             └──────────┘
680  by rw [infinite_neg_iff_infinite_pos_neg, ←neg_pos, ←neg_mul_neg, infinitesimal_neg_iff];
id          └───────────────────────────────┘   └─────┘   └─────────┘  └───────────────────┘
src     └──┘└───────────────────────────────┘└─┘└─────┘└─┘└─────────┘└┘└───────────────────┘
typ     └──┘└───────────────────────────────┘└─┘└─────┘└─┘└─────────┘└┘└───────────────────┘
doc     └──┘                                 └─┘       └─┘           └┘                     
txt     └──┘                                 └─┘       └─┘           └┘                     
par     └──┘                                 └─┘       └─┘           └┘                     
pid       └┘                                 └─┘       └─┘           └┘                     
st     └────────────────────────────────────┘└────────┘└────────────┘└─────────────────────┘└─
681  exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id         └────────────────────────────────────────────────────┘
src  └────┘└────────────────────────────────────────────────────┘
typ  └────┘└────────────────────────────────────────────────────┘
doc  └────┘                                                      
txt  └────┘                                                      
par  └────┘                                                      
pid                                                             
st   ─────────────────────────────────────────────────────────────
682  
src  
typ  
doc  
txt  
par  
pid  
st   
683  lemma infinite_pos_mul_of_not_infinitesimal_neg_infinite_neg {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
684    ¬ infinitesimal x → x < 0 → infinite_neg y → infinite_pos (x * y) :=
id      └───────────┘          └──────────┘    └──────────┘    
src     └───────────┘            └──────────┘     └──────────┘    
typ     └───────────┘          └──────────┘    └──────────┘    
doc      └───────────┘             └──────────┘     └──────────┘
685  λ hx hp hy, by rw mul_comm; exact infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg hy hx hp
id     └┘ └┘ └┘        └──────┘        └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                 └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘      
typ    └┘ └┘ └┘     └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘└┘└┘└┘
doc                 └─┘          └────┘                                                            
txt                 └─┘          └────┘                                                            
par                 └─┘          └────┘                                                            
pid                                                                                              
st                 └───────────────────────────────────────────────────────────────────────────────────
686  
src  
typ  
doc  
txt  
par  
pid  
st   
687  lemma infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
688    infinite_pos x → ¬ infinitesimal y → y < 0 → infinite_neg (x * y) :=
id     └──────────┘     └───────────┘          └──────────┘    
src    └──────────┘      └───────────┘            └──────────┘    
typ    └──────────┘     └───────────┘          └──────────┘    
doc    └──────────┘       └───────────┘             └──────────┘
689  by rw [infinite_neg_iff_infinite_pos_neg, ←neg_pos, neg_mul_eq_mul_neg, infinitesimal_neg_iff];
id          └───────────────────────────────┘   └─────┘  └────────────────┘  └───────────────────┘
src     └──┘└───────────────────────────────┘└─┘└─────┘└┘└────────────────┘└┘└───────────────────┘
typ     └──┘└───────────────────────────────┘└─┘└─────┘└┘└────────────────┘└┘└───────────────────┘
doc     └──┘                                 └─┘       └┘                  └┘                     
txt     └──┘                                 └─┘       └┘                  └┘                     
par     └──┘                                 └─┘       └┘                  └┘                     
pid       └┘                                 └─┘       └┘                  └┘                     
st     └────────────────────────────────────┘└────────┘└──────────────────┘└─────────────────────┘└─
690  exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id         └────────────────────────────────────────────────────┘
src  └────┘└────────────────────────────────────────────────────┘
typ  └────┘└────────────────────────────────────────────────────┘
doc  └────┘                                                      
txt  └────┘                                                      
par  └────┘                                                      
pid                                                             
st   ─────────────────────────────────────────────────────────────
691  
src  
typ  
doc  
txt  
par  
pid  
st   
692  lemma infinite_neg_mul_of_not_infinitesimal_neg_infinite_pos {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
693    ¬ infinitesimal x → x < 0 → infinite_pos y → infinite_neg (x * y) :=
id      └───────────┘          └──────────┘    └──────────┘    
src     └───────────┘            └──────────┘     └──────────┘    
typ     └───────────┘          └──────────┘    └──────────┘    
doc      └───────────┘             └──────────┘     └──────────┘
694  λ hx hp hy, by rw mul_comm; exact infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg hy hx hp
id     └┘ └┘ └┘        └──────┘        └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                 └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘      
typ    └┘ └┘ └┘     └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘└┘└┘└┘
doc                 └─┘          └────┘                                                            
txt                 └─┘          └────┘                                                            
par                 └─┘          └────┘                                                            
pid                                                                                              
st                 └───────────────────────────────────────────────────────────────────────────────────
695  
src  
typ  
doc  
txt  
par  
pid  
st   
696  lemma infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
697    infinite_neg x → ¬ infinitesimal y → 0 < y → infinite_neg (x * y) :=
id     └──────────┘     └───────────┘          └──────────┘    
src    └──────────┘      └───────────┘            └──────────┘    
typ    └──────────┘     └───────────┘          └──────────┘    
doc    └──────────┘       └───────────┘             └──────────┘
698  by rw [infinite_neg_iff_infinite_pos_neg, infinite_neg_iff_infinite_pos_neg, neg_mul_eq_neg_mul];
id          └───────────────────────────────┘  └───────────────────────────────┘  └────────────────┘
src     └──┘└───────────────────────────────┘└┘└───────────────────────────────┘└┘└────────────────┘
typ     └──┘└───────────────────────────────┘└┘└───────────────────────────────┘└┘└────────────────┘
doc     └──┘                                 └┘                                 └┘                  
txt     └──┘                                 └┘                                 └┘                  
par     └──┘                                 └┘                                 └┘                  
pid       └┘                                 └┘                                 └┘                  
st     └────────────────────────────────────┘└─────────────────────────────────┘└──────────────────┘└─
699  exact infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id         └────────────────────────────────────────────────────┘
src  └────┘└────────────────────────────────────────────────────┘
typ  └────┘└────────────────────────────────────────────────────┘
doc  └────┘                                                      
txt  └────┘                                                      
par  └────┘                                                      
pid                                                             
st   ─────────────────────────────────────────────────────────────
700  
src  
typ  
doc  
txt  
par  
pid  
st   
701  lemma infinite_neg_mul_of_not_infinitesimal_pos_infinite_neg {x y : ℝ*} :
id                                                                       └┘
src                                                                      └┘
typ                                                                      └┘
doc                                                                      └┘
702    ¬ infinitesimal x → x > 0 → infinite_neg y → infinite_neg (x * y) :=
id      └───────────┘          └──────────┘    └──────────┘    
src     └───────────┘            └──────────┘     └──────────┘    
typ     └───────────┘          └──────────┘    └──────────┘    
doc      └───────────┘             └──────────┘     └──────────┘
703  λ hx hp hy, by rw mul_comm; exact infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos hy hx hp
id     └┘ └┘ └┘        └──────┘        └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                 └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘      
typ    └┘ └┘ └┘     └─┘└──────┘  └────┘└────────────────────────────────────────────────────┘└┘└┘└┘
doc                 └─┘          └────┘                                                            
txt                 └─┘          └────┘                                                            
par                 └─┘          └────┘                                                            
pid                                                                                              
st                 └───────────────────────────────────────────────────────────────────────────────────
704  
src  
typ  
doc  
txt  
par  
pid  
st   
705  lemma infinite_pos_mul_infinite_pos {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
706    infinite_pos x → infinite_pos y → infinite_pos (x * y) :=
id     └──────────┘    └──────────┘    └──────────┘    
src    └──────────┘     └──────────┘     └──────────┘    
typ    └──────────┘    └──────────┘    └──────────┘    
doc    └──────────┘     └──────────┘     └──────────┘
707  λ hx hy, infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos
id     └┘ └┘  └────────────────────────────────────────────────────┘
src           └────────────────────────────────────────────────────┘
typ    └┘ └┘  └────────────────────────────────────────────────────┘
708  hx (not_infinitesimal_of_infinite_pos hy) (hy 0)
id   └┘  └───────────────────────────────┘ └┘   └┘
src      └───────────────────────────────┘
typ  └┘  └───────────────────────────────┘ └┘   └┘
709  
710  lemma infinite_neg_mul_infinite_neg {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
711    infinite_neg x → infinite_neg y → infinite_pos (x * y) :=
id     └──────────┘    └──────────┘    └──────────┘    
src    └──────────┘     └──────────┘     └──────────┘    
typ    └──────────┘    └──────────┘    └──────────┘    
doc    └──────────┘     └──────────┘     └──────────┘
712  λ hx hy, infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg
id     └┘ └┘  └────────────────────────────────────────────────────┘
src           └────────────────────────────────────────────────────┘
typ    └┘ └┘  └────────────────────────────────────────────────────┘
713  hx (not_infinitesimal_of_infinite_neg hy) (hy 0)
id   └┘  └───────────────────────────────┘ └┘   └┘
src      └───────────────────────────────┘
typ  └┘  └───────────────────────────────┘ └┘   └┘
714  
715  lemma infinite_pos_mul_infinite_neg {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
716    infinite_pos x → infinite_neg y → infinite_neg (x * y) :=
id     └──────────┘    └──────────┘    └──────────┘    
src    └──────────┘     └──────────┘     └──────────┘    
typ    └──────────┘    └──────────┘    └──────────┘    
doc    └──────────┘     └──────────┘     └──────────┘
717  λ hx hy, infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg
id     └┘ └┘  └────────────────────────────────────────────────────┘
src           └────────────────────────────────────────────────────┘
typ    └┘ └┘  └────────────────────────────────────────────────────┘
718  hx (not_infinitesimal_of_infinite_neg hy) (hy 0)
id   └┘  └───────────────────────────────┘ └┘   └┘
src      └───────────────────────────────┘
typ  └┘  └───────────────────────────────┘ └┘   └┘
719  
720  lemma infinite_neg_mul_infinite_pos {x y : ℝ*} :
id                                              └┘
src                                             └┘
typ                                             └┘
doc                                             └┘
721    infinite_neg x → infinite_pos y → infinite_neg (x * y) :=
id     └──────────┘    └──────────┘    └──────────┘    
src    └──────────┘     └──────────┘     └──────────┘    
typ    └──────────┘    └──────────┘    └──────────┘    
doc    └──────────┘     └──────────┘     └──────────┘
722  λ hx hy, infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos
id     └┘ └┘  └────────────────────────────────────────────────────┘
src           └────────────────────────────────────────────────────┘
typ    └┘ └┘  └────────────────────────────────────────────────────┘
723  hx (not_infinitesimal_of_infinite_pos hy) (hy 0)
id   └┘  └───────────────────────────────┘ └┘   └┘
src      └───────────────────────────────┘
typ  └┘  └───────────────────────────────┘ └┘   └┘
724  
725  lemma infinite_mul_of_infinite_not_infinitesimal {x y : ℝ*} :
id                                                           └┘
src                                                          └┘
typ                                                          └┘
doc                                                          └┘
726    infinite x → ¬ infinitesimal y → infinite (x * y) :=
id     └──────┘     └───────────┘    └──────┘    
src    └──────┘      └───────────┘     └──────┘    
typ    └──────┘     └───────────┘    └──────┘    
doc    └──────┘       └───────────┘     └──────┘
727  λ hx hy, have h0 : y < 0 ∨ y > 0 := lt_or_gt_of_ne (λ H0, hy (eq.substr H0 (is_st_refl_real 0))),
id     └┘ └┘                        └────────────┘    └┘  └┘  └───────┘ └┘  └─────────────┘
src                                   └────────────┘            └───────┘     └─────────────┘
typ    └┘ └┘                        └────────────┘    └┘  └┘  └───────┘ └┘  └─────────────┘
728  or.dcases_on hx
id   └──────────┘ └┘
src  └──────────┘
typ  └──────────┘ └┘
729    (or.dcases_on h0
id      └──────────┘ └┘
src     └──────────┘
typ     └──────────┘ └┘
730      (λ H0 Hx, or.inr (infinite_neg_mul_of_infinite_pos_not_infinitesimal_neg Hx hy H0))
id          └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                └────┘  └────────────────────────────────────────────────────┘
typ         └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
731      (λ H0 Hx, or.inl (infinite_pos_mul_of_infinite_pos_not_infinitesimal_pos Hx hy H0)))
id          └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                └────┘  └────────────────────────────────────────────────────┘
typ         └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
732    (or.dcases_on h0
id      └──────────┘ └┘
src     └──────────┘
typ     └──────────┘ └┘
733      (λ H0 Hx, or.inl (infinite_pos_mul_of_infinite_neg_not_infinitesimal_neg Hx hy H0))
id          └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                └────┘  └────────────────────────────────────────────────────┘
typ         └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
734      (λ H0 Hx, or.inr (infinite_neg_mul_of_infinite_neg_not_infinitesimal_pos Hx hy H0)))
id          └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
src                └────┘  └────────────────────────────────────────────────────┘
typ         └┘ └┘  └────┘  └────────────────────────────────────────────────────┘ └┘ └┘ └┘
735  
736  lemma infinite_mul_of_not_infinitesimal_infinite {x y : ℝ*} :
id                                                           └┘
src                                                          └┘
typ                                                          └┘
doc                                                          └┘
737    ¬ infinitesimal x → infinite y → infinite (x * y) :=
id      └───────────┘    └──────┘    └──────┘    
src     └───────────┘     └──────┘     └──────┘    
typ     └───────────┘    └──────┘    └──────┘    
doc      └───────────┘     └──────┘     └──────┘
738  λ hx hy, by rw [mul_comm]; exact infinite_mul_of_infinite_not_infinitesimal hy hx
id     └┘ └┘         └──────┘         └────────────────────────────────────────┘ └┘ └┘
src              └──┘└──────┘  └────┘└────────────────────────────────────────┘    
typ    └┘ └┘     └──┘└──────┘  └────┘└────────────────────────────────────────┘└┘└┘
doc              └──┘          └────┘                                              
txt              └──┘          └────┘                                              
par              └──┘          └────┘                                              
pid                └┘                                                             
st              └───────────┘└────────────────────────────────────────────────────────
739  
src  
typ  
doc  
txt  
par  
pid  
st   
740  lemma infinite_mul_infinite {x y : ℝ*} : infinite x → infinite y → infinite (x * y) :=
id                                      └┘    └──────┘    └──────┘    └──────┘    
src                                     └┘    └──────┘     └──────┘     └──────┘    
typ                                     └┘    └──────┘    └──────┘    └──────┘    
doc                                     └┘    └──────┘     └──────┘     └──────┘
741  λ hx hy, infinite_mul_of_infinite_not_infinitesimal hx (not_infinitesimal_of_infinite hy)
id     └┘ └┘  └────────────────────────────────────────┘ └┘  └───────────────────────────┘ └┘
src           └────────────────────────────────────────┘     └───────────────────────────┘
typ    └┘ └┘  └────────────────────────────────────────┘ └┘  └───────────────────────────┘ └┘
742  
743  end hyperreal